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

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