proposition: Lemma le_minus : forall n k : nat, n - k <= n.
proof: Proof. intros n. induction n as [| n Hrecn]. simpl in |- *. auto. intro k. case k. simpl in |- *. auto. intro k'. simpl in |- *. apply (le_trans n). apply Hrecn. auto. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)