no goals
i a : Nat
h : i < a
⊢ 0 < a - i
induction a with
| zero => contradiction
| succ a ih =>
  match Nat.eq_or_lt_of_le h with
  | Or.inl h => injection h with h; subst h; rw [←Nat.add_one, Nat.add_sub_self_left]; decide
  | Or.inr h =>
    have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
    exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)
no goals
case zero
i : Nat
h : i < zero
⊢ 0 < zero - i
contradiction
no goals
case succ
i a : Nat
ih : i < a → 0 < a - i
h : i < succ a
⊢ 0 < succ a - i
match Nat.eq_or_lt_of_le h with
| Or.inl h => injection h with h; subst h; rw [←Nat.add_one, Nat.add_sub_self_left]; decide
| Or.inr h =>
  have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
  exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < succ a
h : i = a
⊢ 0 < succ a - i
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < succ a
h : succ i = succ a
⊢ 0 < succ a - i
injection h with h
i : Nat
ih : i < i → 0 < i - i
h : i < succ i
⊢ 0 < succ i - i
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < succ a
h : i = a
⊢ 0 < succ a - i
subst h
i : Nat
ih : i < i → 0 < i - i
h : i < succ i
⊢ 0 < 1
i : Nat
ih : i < i → 0 < i - i
h : i < succ i
⊢ 0 < succ i - i
rw [←Nat.add_one, Nat.add_sub_self_left]
no goals
i : Nat
ih : i < i → 0 < i - i
h : i < succ i
⊢ 0 < 1
decide
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < succ a
h : succ i < succ a
this : 0 < a - i
⊢ 0 < succ a - i
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < succ a
h : succ i < succ a
⊢ 0 < succ a - i
have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
no goals
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < succ a
h : succ i < succ a
this : 0 < a - i
⊢ 0 < succ a - i
exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)