proposition: Proposition natminusplusineq (n m : nat) : n <= n - m + m.
proof: Proof. destruct (@leq_dichot m n) as [l | g]. - destruct (symmetric_paths _ _ (natminuspluseq _ _ l)); constructor. - apply n_lt_m_n_leq_m in g. now destruct (symmetric_paths _ _ (sub_leq_0 n m _)). Defined.
imports: Basics Spaces.Nat.Core