x y : PartENat
hx : x ≠ ⊤
h : x ≤ y
⊢ x < y + 1
x y : PartENat
hx : x ≠ ⊤
⊢ x < y + 1 ↔ x ≤ y
refine ⟨le_of_lt_add_one, fun h => ?_⟩
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ y
⊢ ↑m < y + 1
x y : PartENat
hx : x ≠ ⊤
h : x ≤ y
⊢ x < y + 1
rcases ne_top_iff.mp hx with ⟨m, rfl⟩
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
h : ↑m ≤ ⊤
⊢ ↑m < ⊤ + 1

case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ ↑m < ↑n + 1
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ y
⊢ ↑m < y + 1
induction' y using PartENat.casesOn with n
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ m < n + 1
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ ↑m < ↑n + 1
norm_cast
case intro.a.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ m ≤ n
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ m < n + 1
apply Nat.lt_succ_of_le
no goals
case intro.a.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ m ≤ n
norm_cast at h
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
h : ↑m ≤ ⊤
⊢ ↑m < ⊤
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
h : ↑m ≤ ⊤
⊢ ↑m < ⊤ + 1
rw [top_add]
no goals
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
h : ↑m ≤ ⊤
⊢ ↑m < ⊤
apply natCast_lt_top