{ n k : nat } : 0 < n -> 0 < k -> n - k < n. Proof. intros l l'. unfold "<". destruct k, n; try (contradiction (not_lt_zero_r _ _)). simpl; apply leq_succ, sub_less. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.