proposition: Proposition sub_gt_0_lt (n m : nat) : n - m > 0 -> m < n.
proof: Proof. intro ineq. destruct (@leq_dichot n m) as [n_leq_m |]; [ | assumption]. apply sub_leq_0 in n_leq_m. contradiction (not_lt_n_n 0). now rewrite n_leq_m in ineq. Defined.
imports: Basics Spaces.Nat.Core