case none
m n : ℕ
s : psub m n = none
⊢ m < n

case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
m n : ℕ
⊢ psub m n = none ↔ m < n
cases s : psub m n <;> simp [eq_comm]
case none
m n : ℕ
s : psub m n = none
⊢ m < n
case none
m n : ℕ
s : psub m n = none
⊢ m < n
show m < n
case none
m n : ℕ
s : psub m n = none
h : m ≥ n
⊢ False
case none
m n : ℕ
s : psub m n = none
⊢ m < n
refine' lt_of_not_ge fun h => _
case none.intro
m n : ℕ
s : psub m n = none
h : m ≥ n
k : ℕ
e : n + k = m
⊢ False
case none
m n : ℕ
s : psub m n = none
h : m ≥ n
⊢ False
cases' le.dest h with k e
no goals
case none.intro
m n : ℕ
s : psub m n = none
h : m ≥ n
k : ℕ
e : n + k = m
⊢ False
injection s.symm.trans (psub_eq_some.2 <| (add_comm _ _).trans e)
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
show n ≤ m
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ val✝ + n
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
rw [← psub_eq_some.1 s]
no goals
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ val✝ + n
apply Nat.le_add_left