i j : Nat
h : i < j
⊢ j - (i + 1 + 1) < j - i
i j : Nat
h : i < j
⊢ j - 1 - (i + 1) < j - i
rw [Nat.sub_sub, Nat.add_comm]
no goals
i j : Nat
h : i < j
⊢ j - (i + 1 + 1) < j - i
exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)