proposition: Proposition sub_less { n k : nat } : n - k <= n.
proof: Proof. revert k. simple_induction n n IHn. - intros; apply leq_0_n. - destruct k. + apply leq_n. + simpl; apply (@leq_trans _ n _); [ apply IHn | apply leq_S, leq_n]. Defined.
imports: Basics Spaces.Nat.Core