a i : Nat
h : i < a
⊢ pred (a - i) < a - i
a i : Nat
h : i < a
⊢ a - (i + 1) < a - i
rw [Nat.add_succ, Nat.sub_succ]
case a
a i : Nat
h : i < a
⊢ a - i ≠ 0
a i : Nat
h : i < a
⊢ pred (a - i) < a - i
apply Nat.pred_lt
case a.h
a i : Nat
h : i < a
⊢ ?a.b✝ < a - i

case a.b
a i : Nat
h : i < a
⊢ Nat
case a
a i : Nat
h : i < a
⊢ a - i ≠ 0
apply Nat.not_eq_zero_of_lt
case a.h.h
a i : Nat
h : i < a
⊢ i < a
case a.h
a i : Nat
h : i < a
⊢ ?a.b✝ < a - i

case a.b
a i : Nat
h : i < a
⊢ Nat
apply Nat.zero_lt_sub_of_lt
no goals
case a.h.h
a i : Nat
h : i < a
⊢ i < a
assumption