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

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