{ n k : nat } : n - k <= n. Proof. revert k. simple_induction n n IHn. - intros; apply leq_zero_l. - destruct k. + apply leq_refl. + simpl; apply (@leq_trans _ n _); [ apply IHn | apply leq_succ_r, leq_refl]. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.