i n : Nat
h : i < n
⊢ n - (1 + i) < n
i n : Nat
h : i < n
⊢ n - 1 - i < n
rw [Nat.sub_sub]
i n : Nat
h : i < n
⊢ 0 < 1 + i
i n : Nat
h : i < n
⊢ n - (1 + i) < n
apply Nat.sub_lt (Nat.lt_of_lt_of_le (Nat.zero_lt_succ _) h)
i n : Nat
h : i < n
⊢ 0 < i + 1
i n : Nat
h : i < n
⊢ 0 < 1 + i
rw [Nat.add_comm]
no goals
i n : Nat
h : i < n
⊢ 0 < i + 1
apply Nat.zero_lt_succ