case intro
y z : PartENat
hz : z ≠ ⊤
m : ℕ
h : ↑m < y
⊢ ↑m + z < y + z
x y z : PartENat
h : x < y
hz : z ≠ ⊤
⊢ x + z < y + z
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩
case intro.intro
y : PartENat
m : ℕ
h : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
⊢ ↑m + ↑k < y + ↑k
case intro
y z : PartENat
hz : z ≠ ⊤
m : ℕ
h : ↑m < y
⊢ ↑m + z < y + z
rcases ne_top_iff.mp hz with ⟨k, rfl⟩
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤ + ↑k

case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : ↑m < ↑n
⊢ ↑m + ↑k < ↑n + ↑k
case intro.intro
y : PartENat
m : ℕ
h : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
⊢ ↑m + ↑k < y + ↑k
induction' y using PartENat.casesOn with n
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ ↑m + ↑k < ↑n + ↑k
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : ↑m < ↑n
⊢ ↑m + ↑k < ↑n + ↑k
norm_cast at h
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ m + k < n + k
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ ↑m + ↑k < ↑n + ↑k
norm_cast
no goals
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ m + k < n + k
apply add_lt_add_right h
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤ + ↑k
rw [top_add]
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑(m + k) < ⊤
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤
norm_cast
no goals
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑(m + k) < ⊤
apply natCast_lt_top