+theorem lt_minus_l: \forall m,l,n:nat.
+ l < m \to m \le n \to n - m < n - l.
+apply nat_elim2
+ [intros.apply False_ind.apply (not_le_Sn_O ? H)
+ |intros.autobatch.
+ (* rewrite < minus_n_O.
+ change in H1 with (n<n1);
+ apply lt_minus_m; autobatch depth=2; *)
+ |intros.
+ generalize in match H2.
+ apply (nat_case n1)
+ [intros.apply False_ind.apply (not_le_Sn_O ? H3)
+ |intros.simplify.
+ apply H
+ [
+ apply lt_S_S_to_lt.
+ assumption
+ |apply le_S_S_to_le.assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem lt_minus_r: \forall n,m,l:nat.
+ n \le l \to l < m \to l -n < m -n.
+ unfold lt.
+intro.elim n
+ [applyS H1
+ |(*
+ letin x ≝ (lt_pred (l-n1) (m-n1)).
+ clearbody x.
+ unfold lt in x.
+ autobatch depth=4 width=5 size=10 by
+ x, H, H1, H2, trans_le, le_n_Sn, le_n.
+ ]*)
+ rewrite > eq_minus_S_pred.
+ rewrite > eq_minus_S_pred.
+ apply lt_pred
+ [unfold lt.apply le_plus_to_minus_r.applyS H1
+ |apply H[autobatch depth=2|assumption]
+ ]
+ ]
+qed.
+
+lemma lt_to_lt_O_minus : \forall m,n.
+ n < m \to O < m - n.
+intros.
+unfold. apply le_plus_to_minus_r. unfold in H.
+cut ((S n ≤ m) = (1 + n ≤ m)) as applyS;
+ [ rewrite < applyS; assumption;
+ | demodulate; reflexivity. ]
+(*
+rewrite > sym_plus.
+rewrite < plus_n_Sm.
+rewrite < plus_n_O.
+assumption.
+*)
+qed.
+