proposition: Proposition i_lt_n_sum_m (n m i : nat) : i < n - m -> m <= n.
proof: Proof. revert m i; simple_induction n n IHn. - intros m i l. simpl in l. contradiction (not_lt_n_0 _ _). - intros m i l. destruct m. + apply leq_0_n. + apply leq_S_n'. simpl in l. apply (IHn m i l). Defined.
imports: Basics Spaces.Nat.Core