no goals
a i : Nat
⊢ a - i ≤ succ a - i
cases i with
| zero => apply Nat.le_of_lt; apply Nat.lt_succ_self
| succ i => rw [Nat.sub_succ, Nat.succ_sub_succ]; apply Nat.pred_le
case zero.h
a : Nat
⊢ a - zero < succ a - zero
case zero
a : Nat
⊢ a - zero ≤ succ a - zero
apply Nat.le_of_lt
no goals
case zero.h
a : Nat
⊢ a - zero < succ a - zero
apply Nat.lt_succ_self
case succ
a i : Nat
⊢ pred (a - i) ≤ a - i
case succ
a i : Nat
⊢ a - succ i ≤ succ a - succ i
rw [Nat.sub_succ, Nat.succ_sub_succ]
no goals
case succ
a i : Nat
⊢ pred (a - i) ≤ a - i
apply Nat.pred_le