Definition minusplusnmmineq (n m : nat) : (n - m) + m ≥ n. Proof. intros. induction (natlthorgeh n m) as [ lt | ge ]. - rewrite (minuseq0 _ _ (natlthtoleh _ _ lt)). apply (natgthtogeh _ _ lt). - rewrite (minusplusnmm _ _ ge). apply isreflnatgeh. Defined.