no goals
n m : Nat
⊢ n - m ≤ n
induction m with
| zero      => exact Nat.le_refl (n - 0)
| succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
no goals
case zero
n : Nat
⊢ n - zero ≤ n
exact Nat.le_refl (n - 0)
no goals
case succ
n m : Nat
ih : n - m ≤ n
⊢ n - succ m ≤ n
apply Nat.le_trans (pred_le (n - m)) ih