+theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
+intros.apply nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))).
+intro.elim n1.simplify.apply le_n_Sn.
+simplify.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n_Sn.
+intros.simplify.apply H.
+qed.
+
+theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
+intros 3.simplify.intro.
+apply trans_le (m-n) (S (m-(S n))) p.
+apply minus_le_S_minus_S.
+assumption.
+qed.
+
+theorem le_minus_m: \forall n,m:nat. n-m \leq n.
+intros.apply nat_elim2 (\lambda m,n. n-m \leq n).
+intros.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n.
+intros.simplify.apply le_S.assumption.
+qed.
+
+theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
+intros.apply lt_O_n_elim n H.intro.
+apply lt_O_n_elim m H1.intro.
+simplify.apply le_S_S.apply le_minus_m.
+qed.
+
+theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
+intros 2.
+apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m).
+intros.apply le_O_n.
+simplify.intros. assumption.
+simplify.intros.apply le_S_S.apply H.assumption.
+qed.
+
+(* galois *)
+theorem monotonic_le_minus_r:
+\forall p,q,n:nat. q \leq p \to n-p \le n-q.
+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.
+qed.
+
+theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
+intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m))).
+intros.apply le_O_n.
+simplify.intros.rewrite < plus_n_O.assumption.