(n m : nat) : n <= n - m + m. Proof. destruct (@leq_dichotomy m n) as [l | gt]. - rewrite <- nat_sub_l_add_l; trivial. destruct (nat_add_sub_cancel_r n m)^. apply leq_refl; done. - apply leq_lt in gt. destruct (equiv_nat_sub_leq _)^. assumption. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.