proposition: Proposition nat_sub_add_ineq (n m : nat) : n <= n - m + m.
proof: Proof. destruct (@leq_dichot m n) as [l | gt]. - destruct (symmetric_paths _ _ (nataddsub_comm _ _ m l)). destruct (symmetric_paths _ _ (add_n_sub_n_eq n m)). apply leq_refl; done. - apply n_lt_m_n_leq_m in gt. destruct (symmetric_paths _ _ (sub_leq_0 n m _)). assumption. Defined.
imports: Basics Spaces.Nat.Core