n m : ℕ
h : n < succ m
this✝ : n ≤ m
this : succ (n + n) ≤ succ (m + m)
⊢ succ (n + n) ≤ succ (m + m)
n m : ℕ
h : n < succ m
this✝ : n ≤ m
this : succ (n + n) ≤ succ (m + m)
⊢ succ (n + n) ≤ succ m + m
rw [succ_add]
no goals
n m : ℕ
h : n < succ m
this✝ : n ≤ m
this : succ (n + n) ≤ succ (m + m)
⊢ succ (n + n) ≤ succ (m + m)
assumption