-simplify.intros 2.apply (nat_elim2
-(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
-intros.apply (le_n_O_elim n H).apply le_n.
-intros.rewrite < minus_n_O.
-apply le_minus_m.
-intros.elim a.simplify.apply le_n.
-simplify.apply H.apply le_S_S_to_le.assumption.
+intros 2.apply (nat_elim2 ???? p q); intros;
+ [apply (le_n_O_elim n H).apply le_n.
+ |applyS le_minus_m.
+ |elim n1;intros;[apply le_n|simplify.apply H.apply le_S_S_to_le.assumption]
+ ]
+qed.
+
+theorem monotonic_le_minus_l:
+∀p,q,n:nat. q \leq p \to q-n \le p-n.
+intros 2.apply (nat_elim2 ???? p q); intros;
+ [apply (le_n_O_elim n H).apply le_n.
+ |apply le_O_n.
+ |cases n1;[apply H1|simplify. apply H.apply le_S_S_to_le.assumption]
+ ]