X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=7945a76e01c3c36ebe2d68ad3eda850af1bf4186;hb=3a12950125e7a4a792546aacea40505f3cecae89;hp=1b790031401c2aeb8dc04a3ad769fd9f43fa86c6;hpb=7bbce6bc163892cfd99cfcda65db42001b86789f;p=helm.git

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 1b7900314..7945a76e0 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -131,15 +131,80 @@ apply le_S.assumption.
 apply lt_to_le.assumption.
 qed.
 
-(*
-theorem le_plus_minus: \forall n,m,p. n+m \leq p \to n \leq p-m.
-intros 3.
-elim p.simplify.apply trans_le ? (n+m) ?.
-elim sym_plus ? ?.
-apply plus_le.assumption.
-apply le_n_Sm_elim ? ? H1.
+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 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.
 intros.
-*)
+rewrite < plus_n_Sm.
+apply le_S_S.apply H.
+exact H1.
+qed.
+
+theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
+intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)).
+intros.simplify.apply le_O_n.
+intros 2.rewrite < plus_n_O.intro.simplify.assumption.
+intros.simplify.apply H.
+apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
+qed.
+
+(* the converse of le_plus_to_minus does not hold *)
+theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
+intros 3.apply nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))).
+intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
+intro.intro.cut n=O.rewrite > Hcut.apply le_O_n.
+apply sym_eq. apply le_n_O_to_eq.
+apply trans_le ? (n+(S n1)).
+rewrite < sym_plus.
+apply le_plus_n.assumption.
+intros.simplify.
+apply H.apply le_S_S_to_le.
+rewrite > plus_n_Sm.assumption.
+qed.
+
 
 theorem distributive_times_minus: distributive nat times minus.
 simplify.
@@ -149,7 +214,7 @@ cut x*(y-z)+x*z = (x*y-x*z)+x*z.
 apply inj_plus_l (x*z).
 assumption.
 apply trans_eq nat ? (x*y).
-rewrite < times_plus_distr. 
+rewrite < distr_times_plus. 
 rewrite < plus_minus_m_m ? ? H.reflexivity.
 rewrite < plus_minus_m_m ? ? ?.reflexivity.
 apply le_times_r.
@@ -167,8 +232,3 @@ qed.
 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 \def distributive_times_minus.
 
-theorem le_minus_m: \forall n,m:nat. n-m \leq n.
-intro.elim n.simplify.apply le_n.
-elim m.simplify.apply le_n.
-simplify.apply le_S.apply H.
-qed.