X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2Fnat.ma;h=3152b0dbe3503aeee43bbd0f872b847f87979239;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=8efe32043339fc033900d6495826b2b96d6d17fe;hpb=a356482acf3bf92eaa34d2b38ee2e81761f58520;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 8efe32043..3152b0dbe 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -262,41 +262,91 @@ ntheorem le_pred_n : ∀n:nat. pred n ≤ n.
 ntheorem monotonic_pred: monotonic ? le pred.
 #n; #m; #lenm; nelim lenm; /2/; nqed.
 
-ntheorem le_S_S_to_le : ∀n,m:nat. S n ≤ S m → n ≤ m.
+ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
 /2/; nqed.
 
-(*
-nchange with (pred (S n) ≤ pred (S m));
-nelim leSS; apply le_n.apply (trans_le ? (pred n1)).assumption.
-apply le_pred_n.
-qed.
+ntheorem lt_S_S_to_lt: ∀n,m. S n < S m \to n < m.
+/2/; nqed. 
 
-theorem lt_S_S_to_lt: \forall n,m. 
-  S n < S m \to n < m.
-intros. apply le_S_S_to_le. assumption.
-qed.
+ntheorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
+/2/; nqed.
 
-theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
-intros;
-unfold lt in H;
-apply (le_S_S ? ? H).
-qed.
+ntheorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
+#n; #m; #Hlt; nelim Hlt;//; nqed.
 
-theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
-intros.elim H.exact I.exact I.
-qed.
+(* lt vs. le *)
+ntheorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
+#n; #Hlen0; napply (lt_to_not_zero ?? Hlen0); nqed.
 
-(* not le *)
-theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
-intros.unfold Not.simplify.intros.apply (leS_to_not_zero ? ? H).
-qed.
+ntheorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
+/3/; nqed.
 
-theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
-intros.elim n.apply not_le_Sn_O.unfold Not.simplify.intros.cut (S n1 \leq n1).
-apply H.assumption.
-apply le_S_S_to_le.assumption.
-qed.
+ntheorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
+/3/; nqed.
+
+ntheorem decidable_le: ∀n,m. decidable (n≤m).
+napply nat_elim2; #n; /2/;
+#m; #dec; ncases dec;/3/; nqed.
+
+ntheorem decidable_lt: ∀n,m. decidable (n < m).
+#n; #m; napply decidable_le ; nqed.
+
+ntheorem not_le_Sn_n: ∀n:nat. S n ≰ n.
+#n; nelim n; /2/; nqed.
+
+ntheorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
+/2/; nqed.
+
+ntheorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
+napply nat_elim2; #n;
+ ##[#abs; napply False_ind;/2/;
+ ##|/2/;
+ ##|#m;#Hind;#HnotleSS; napply lt_to_lt_S_S;/3/;
+ ##]
+nqed.
+
+ntheorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
+#n; #m; #Hltnm; nelim Hltnm;/3/; nqed.
+
+ntheorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
+#n; #m; #Hnlt; napply lt_S_to_le;
+(* something strange here: /2/ fails: 
+   we need an extra depths for unfolding not *)
+napply not_le_to_lt; napply Hnlt; nqed. 
+
+ntheorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
+/2/; nqed.
+
+(* lt and le trans *)
+
+ntheorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
+#n; #m; #p; #H; #H1; nelim H1; /2/; nqed.
 
+ntheorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
+#n; #m; #p; #H; nelim H; /3/; nqed.
+
+ntheorem lt_S_to_lt: ∀n,m. S n < m → n < m.
+/2/; nqed.
+
+ntheorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
+/2/; nqed.
+
+(*
+theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
+(S O) \lt n \to O \lt (pred n).
+intros.
+apply (ltn_to_ltO (pred (S O)) (pred n) ?).
+ apply (lt_pred (S O) n);
+ [ apply (lt_O_S O) 
+ | assumption
+ ]
+qed. *)
+
+ntheorem lt_O_n_elim: ∀n:nat. O < n → 
+  ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
+#n; nelim n; //; #abs; napply False_ind; /2/; nqed.
+
+(*
 theorem lt_pred: \forall n,m. 
   O < n \to n < m \to pred n < pred m. 
 apply nat_elim2
@@ -325,48 +375,18 @@ elim n;
 ].
 qed.
 
-theorem le_to_le_pred:
- ∀n,m. n ≤ m → pred n ≤ pred m.
-intros 2;
-elim n;
-[ simplify;
-  apply le_O_n
-| simplify;
-  elim m in H1 ⊢ %;
-  [ elim (not_le_Sn_O ? H1)
-  | simplify;
-    apply le_S_S_to_le;
-    assumption
-  ]
-].
-qed.
+*)
 
 (* le to lt or eq *)
-theorem le_to_or_lt_eq : \forall n,m:nat. 
-n \leq m \to n < m \lor n = m.
-intros.elim H.
-right.reflexivity.
-left.unfold lt.apply le_S_S.assumption.
-qed.
-
-theorem Not_lt_n_n: ∀n. n ≮ n.
-intro;
-unfold Not;
-intro;
-unfold lt in H;
-apply (not_le_Sn_n ? H).
-qed.
+ntheorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
+#n; #m; #lenm; nelim lenm; /3/; nqed.
 
 (* not eq *)
-theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
-unfold Not.intros.cut ((le (S n) m) \to False).
-apply Hcut.assumption.rewrite < H1.
-apply not_le_Sn_n.
-qed.
+ntheorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
+/2/; nqed.
 
-(*not lt*)
-theorem eq_to_not_lt: \forall a,b:nat.
-a = b \to a \nlt b.
+(*not lt 
+ntheorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
 intros.
 unfold Not.
 intros.
@@ -375,7 +395,7 @@ apply (lt_to_not_eq b b)
 [ assumption
 | reflexivity
 ]
-qed.
+qed. 
 
 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
 intros;
@@ -388,133 +408,32 @@ intro;
 generalize in match (transitive_le ? ? ? H2 H1);
 intro;
 apply (not_le_Sn_n ? H3).
-qed.
-
-(* le vs. lt *)
-theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
-simplify.intros.unfold lt in H.elim H.
-apply le_S. apply le_n.
-apply le_S. assumption.
-qed.
-
-theorem lt_S_to_le : \forall n,m:nat. n < S m \to n \leq m.
-simplify.intros.
-apply le_S_S_to_le.assumption.
-qed.
-
-theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
-intros 2.
-apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n)).
-intros.apply (absurd (O \leq n1)).apply le_O_n.assumption.
-unfold Not.unfold lt.intros.apply le_S_S.apply le_O_n.
-unfold Not.unfold lt.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
-assumption.
-qed.
-
-theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
-unfold Not.unfold lt.intros 3.elim H.
-apply (not_le_Sn_n n H1).
-apply H2.apply lt_to_le. apply H3.
-qed.
-
-theorem not_lt_to_le: \forall n,m:nat. Not (lt n m) \to le m n.
-simplify.intros.
-apply lt_S_to_le.
-apply not_le_to_lt.exact H.
-qed.
+qed. *)
 
-theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
-intros.unfold Not.unfold lt.
-apply lt_to_not_le.unfold lt.
-apply le_S_S.assumption.
-qed.
-
-theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
-intros;
-elim (le_to_or_lt_eq ? ? H1);
-[ assumption
-| elim (H H2)
-].
-qed.
+ntheorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
+#n; #m; #Hneq; #Hle; ncases (le_to_or_lt_eq ?? Hle); //;
+#Heq; nelim (Hneq Heq); nqed.
 
 (* le elimination *)
-theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
-intro.elim n.reflexivity.
-apply False_ind.
-apply not_le_Sn_O;
-[2: apply H1 | skip].
-qed.
+ntheorem le_n_O_to_eq : ∀n:nat. n ≤ O → O=n.
+#n; ncases n; //; #a ; #abs; nelim (not_le_Sn_O ? abs); nqed.
 
-theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
-P O \to P n.
-intro.elim n.
-assumption.
-apply False_ind.
-apply  (not_le_Sn_O ? H1).
-qed.
+ntheorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
+#n; ncases n; //; #a; #abs; nelim (not_le_Sn_O ? abs); nqed. 
 
-theorem le_n_Sm_elim : \forall n,m:nat.n \leq S m \to 
-\forall P:Prop. (S n \leq S m \to P) \to (n=S m \to P) \to P.
-intros 4.elim H.
-apply H2.reflexivity.
-apply H3. apply le_S_S. assumption.
-qed.
+ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m → 
+∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
+#n; #m; #Hle; #P; nelim Hle; /3/; nqed.
 
 (* le and eq *)
-lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
-apply nat_elim2
-  [intros.apply le_n_O_to_eq.assumption
-  |intros.apply sym_eq.apply le_n_O_to_eq.assumption
-  |intros.apply eq_f.apply H
-    [apply le_S_S_to_le.assumption
-    |apply le_S_S_to_le.assumption
-    ]
-  ]
-qed.
 
-(* lt and le trans *)
-theorem lt_O_S : \forall n:nat. O < S n.
-intro. unfold. apply le_S_S. apply le_O_n.
-qed.
+ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
+napply nat_elim2; /3/; nqed.
 
-theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
-intros.elim H1.
-assumption.unfold lt.apply le_S.assumption.
-qed.
-
-theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
-intros 4.elim H.
-assumption.apply H2.unfold lt.
-apply lt_to_le.assumption.
-qed.
-
-theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
-intros.
-apply (trans_lt ? (S n))
-  [apply le_n|assumption]
-qed.
-
-theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
-intros.apply (le_to_lt_to_lt O n).
-apply le_O_n.assumption.
-qed.
-
-theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
-(S O) \lt n \to O \lt (pred n).
-intros.
-apply (ltn_to_ltO (pred (S O)) (pred n) ?).
- apply (lt_pred (S O) n);
- [ apply (lt_O_S O) 
- | assumption
- ]
-qed.
-
-theorem lt_O_n_elim: \forall n:nat. lt O n \to 
-\forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
-intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
-apply H2.
-qed.
+ntheorem lt_O_S : \forall n:nat. O < S n.
+/2/; nqed.
 
+(*
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.
 unfold antisymmetric.intros 2.
@@ -537,38 +456,27 @@ intro;
 apply antisym_le;
 assumption.
 qed.
-
-theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
-intros.
-apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).
-intros.unfold decidable.left.apply le_O_n.
-intros.unfold decidable.right.exact (not_le_Sn_O n1).
-intros 2.unfold decidable.intro.elim H.
-left.apply le_S_S.assumption.
-right.unfold Not.intro.apply H1.apply le_S_S_to_le.assumption.
-qed.
-
-theorem decidable_lt: \forall n,m:nat. decidable (n < m).
-intros.exact (decidable_le (S n) m).
-qed.
+*)
 
 (* well founded induction principles *)
 
-theorem nat_elim1 : \forall n:nat.\forall P:nat \to Prop. 
-(\forall m.(\forall p. (p \lt m) \to P p) \to P m) \to P n.
-intros.cut (\forall q:nat. q \le n \to P q).
-apply (Hcut n).apply le_n.
-elim n.apply (le_n_O_elim q H1).
-apply H.
-intros.apply False_ind.apply (not_le_Sn_O p H2).
-apply H.intros.apply H1.
-cut (p < S n1).
-apply lt_S_to_le.assumption.
-apply (lt_to_le_to_lt p q (S n1) H3 H2).
-qed.
+ntheorem nat_elim1 : ∀n:nat.∀P:nat → Prop. 
+(∀m.(∀p. p < m → P p) → P m) → P n.
+#n; #P; #H; 
+ncut (∀q:nat. q ≤ n → P q);/2/;
+nelim n; 
+ ##[#q; #HleO; (* applica male *) 
+    napply (le_n_O_elim ? HleO);
+    napply H; #p; #ltpO;
+    napply False_ind; /2/; 
+ ##|#p; #Hind; #q; #HleS; 
+    napply H; #a; #lta; napply Hind;
+    napply le_S_S_to_le;/2/;
+ ##]
+nqed.
 
 (* some properties of functions *)
-
+(*
 definition increasing \def \lambda f:nat \to nat. 
 \forall n:nat. f n < f (S n).
 
@@ -620,3 +528,268 @@ apply H.
 apply le_to_or_lt_eq.apply H6.
 qed.
 *)
+
+(*********************** monotonicity ***************************)
+ntheorem monotonic_le_plus_r: 
+∀n:nat.monotonic nat le (λm.n + m).
+#n; #a; #b; nelim n; nnormalize; //;
+#m; #H; #leab;napply le_S_S; /2/; nqed.
+
+(*
+ntheorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
+≝ monotonic_le_plus_r. *)
+
+ntheorem monotonic_le_plus_l: 
+∀m:nat.monotonic nat le (λn.n + m).
+/2/; nqed.
+
+(*
+ntheorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
+\def monotonic_le_plus_l. *)
+
+ntheorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  \to m1 ≤ m2 
+→ n1 + m1 ≤ n2 + m2.
+#n1; #n2; #m1; #m2; #len; #lem; napply transitive_le;
+/2/; nqed.
+
+ntheorem le_plus_n :∀n,m:nat. m ≤ n + m.
+/2/; nqed. 
+
+ntheorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
+/2/; nqed.
+
+ntheorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
+//; nqed.
+
+ntheorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
+#a; nelim a; /3/; nqed. 
+
+ntheorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
+/2/; nqed. 
+
+(* times *)
+ntheorem monotonic_le_times_r: 
+∀n:nat.monotonic nat le (λm. n * m).
+#n; #x; #y; #lexy; nelim n; nnormalize;//;(* lento /2/;*)
+#a; #lea; napply le_plus; //;
+nqed.
+
+(*
+ntheorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
+\def monotonic_le_times_r. *)
+
+ntheorem monotonic_le_times_l: 
+∀m:nat.monotonic nat le (λn.n*m).
+/2/; nqed.
+
+(*
+theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
+\def monotonic_le_times_l. *)
+
+ntheorem le_times: ∀n1,n2,m1,m2:nat. 
+n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
+#n1; #n2; #m1; #m2; #len; #lem; 
+napply transitive_le; (* /2/ slow *)
+ ##[ ##| napply monotonic_le_times_l;//; 
+     ##| napply monotonic_le_times_r;//;
+ ##]
+nqed.
+
+ntheorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
+(* bello *)
+/2/; nqed.
+
+ntheorem le_times_to_le: 
+∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
+#a; napply nat_elim2; nnormalize;
+  ##[//;
+  ##|#n; #H1; #H2; napply False_ind;
+     ngeneralize in match H2;
+     napply lt_to_not_le;
+     napply (transitive_le ? (S n));/2/;
+  ##|#n; #m; #H; #lta; #le;
+     napply le_S_S; napply H; /2/;
+  ##]
+nqed.
+
+ntheorem le_S_times_2: ∀n,m.O < m → n ≤ m → n < 2*m.
+#n; #m; #posm; #lenm; (* interessante *)
+nnormalize; napplyS (le_plus n); //; nqed.
+
+(************************** minus ******************************)
+
+nlet rec minus n m ≝ 
+ match n with 
+ [ O ⇒ O
+ | S p ⇒ 
+	match m with
+	  [ O ⇒ S p
+    | S q ⇒ minus p q ]].
+        
+interpretation "natural minus" 'minus x y = (minus x y).
+
+ntheorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
+//; nqed.
+
+ntheorem minus_O_n: ∀n:nat.O=O-n.
+#n; ncases n; //; nqed.
+
+ntheorem minus_n_O: ∀n:nat.n=n-O.
+#n; ncases n; //; nqed.
+
+ntheorem minus_n_n: ∀n:nat.O=n-n.
+#n; nelim n; //; nqed.
+
+ntheorem minus_Sn_n: ∀n:nat. S O = (S n)-n.
+#n; nelim n; //; nqed.
+
+ntheorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
+(* qualcosa da capire qui 
+#n; #m; #lenm; nelim lenm; napplyS refl_eq. *)
+napply nat_elim2; 
+  ##[//
+  ##|#n; #abs; napply False_ind;/2/;
+  ##|/3/;
+  ##]
+nqed.
+
+ntheorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
+napply nat_elim2; //; nqed.
+
+ntheorem plus_minus:
+∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
+napply nat_elim2; 
+  ##[//
+  ##|#n; #p; #abs; napply False_ind;/2/;
+  ##|nnormalize;/3/;
+  ##]
+nqed.
+
+ntheorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
+#n; #m; napplyS (plus_minus m m n); //; nqed.
+
+ntheorem plus_minus_m_m: ∀n,m:nat.
+m \leq n \to n = (n-m)+m.
+#n; #m; #lemn; napplyS symmetric_eq; 
+napplyS (plus_minus m n m); //; nqed.
+
+ntheorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
+#n; nelim n;
+  ##[//
+  ##|#a; #Hind; #m; ncases m;/2/;  
+  ##]
+nqed.
+
+ntheorem minus_to_plus :∀n,m,p:nat.
+  m ≤ n → n-m = p → n = m+p.
+#n; #m; #p; #lemn; #eqp; napplyS plus_minus_m_m; //;
+nqed.
+
+ntheorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
+(* /4/ done in 43.5 *)
+#n; #m; #p; #eqp; 
+napply symmetric_eq;
+napplyS (minus_plus_m_m p m);
+nqed.
+
+ntheorem minus_pred_pred : ∀n,m:nat. O < n → O < m → 
+pred n - pred m = n - m.
+#n; #m; #posn; #posm;
+napply (lt_O_n_elim n posn);
+napply (lt_O_n_elim m posm);//.
+nqed.
+
+(*
+theorem eq_minus_n_m_O: \forall n,m:nat.
+n \leq m \to n-m = O.
+intros 2.
+apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
+intros.simplify.reflexivity.
+intros.apply False_ind.
+apply not_le_Sn_O;
+[2: apply H | skip].
+intros.
+simplify.apply H.apply le_S_S_to_le. apply H1.
+qed.
+
+theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
+intros.elim H.elim (minus_Sn_n n).apply le_n.
+rewrite > minus_Sn_m.
+apply le_S.assumption.
+apply lt_to_le.assumption.
+qed.
+
+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.intro.
+(* autobatch *)
+(* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
+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.unfold lt.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.
+*)
+
+(* monotonicity and galois *)
+
+ntheorem monotonic_le_minus_l: 
+∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
+napply nat_elim2; #p; #q;
+  ##[#lePO; napply (le_n_O_elim ? lePO);//;
+  ##|//;
+  ##|#Hind; #n; ncases n;
+    ##[//;
+    ##|#a; #leSS; napply Hind; /2/;
+    ##]
+  ##]
+nqed.
+
+ntheorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
+#n; #m; #p; #lep;
+napply transitive_le;
+  ##[##|napply le_plus_minus_m_m
+  ##|napply monotonic_le_plus_l;//;
+  ##]
+nqed.
+
+ntheorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
+#n; #m; #p; #lep;
+(* bello *)
+napplyS monotonic_le_minus_l;//;
+nqed.
+
+ntheorem monotonic_le_minus_r: 
+∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
+#p; #q; #n; #lepq;
+napply le_plus_to_minus;
+napply (transitive_le ??? (le_plus_minus_m_m ? q));/2/;
+nqed.