case a
x y : PartENat
h✝ : x < y
h : x < ⊤
⊢ x + 1 ≤ ⊤

case a
x y : PartENat
h✝ : x < y
n : ℕ
h : x < ↑n
⊢ x + 1 ≤ ↑n
x y : PartENat
h : x < y
⊢ x + 1 ≤ y
induction' y using PartENat.casesOn with n
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ ↑m + 1 ≤ ↑n
case a
x y : PartENat
h✝ : x < y
n : ℕ
h : x < ↑n
⊢ x + 1 ≤ ↑n
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ m + 1 ≤ n
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ ↑m + 1 ≤ ↑n
norm_cast
case a.intro.h
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ m < n
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ m + 1 ≤ n
apply Nat.succ_le_of_lt
no goals
case a.intro.h
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ m < n
norm_cast at h
no goals
case a
x y : PartENat
h✝ : x < y
h : x < ⊤
⊢ x + 1 ≤ ⊤
apply le_top