proposition: Proposition sub_less_strict { n k : nat } : 0 < n -> 0 < k -> n - k < n.
proof: Proof. intros l l'. unfold "<". destruct k, n; try (contradiction (not_lt_n_0 _ _)). simpl; apply leq_S_n', sub_less. Defined.
imports: Basics Spaces.Nat.Core