proposition: Proposition lt_sub_gt_0 (n m : nat) : m < n -> 0 < n - m.
proof: Proof. revert m; simple_induction n n IHn. - intros m ineq. contradiction (not_lt_n_0 m). - destruct m. + simpl. easy. + simpl. intro ineq. apply leq_S_n in ineq. now apply IHn in ineq. Defined.
imports: Basics Spaces.Nat.Core