X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_group.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_group.ma;h=7f66d3b80b291946dcb441629db4cbb752401b8d;hb=a1f4ef3daaeed7a3121a40afe55f321565669da8;hp=d2f96fb5c7c03faf6fdb1b76774fd49dd8c86c14;hpb=f86ba51fa84583b5963fca03687cd23b838a99f5;p=helm.git

diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index d2f96fb5c..7f66d3b80 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -123,6 +123,19 @@ apply (le_rewr ??? (-z+(z+y)) (plus_assoc ????));
 apply (fle_plusl ??? (-z) L);
 qed.
 
+lemma plus_cancl_lt: 
+  ∀G:ogroup.∀x,y,z:G.z+x < z+y → x < y.
+intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancl_le; assumption]
+apply (plus_cancl_ap ???? LE);
+qed.
+
+lemma plus_cancr_lt: 
+  ∀G:ogroup.∀x,y,z:G.x+z < y+z → x < y.
+intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancr_le; assumption]
+apply (plus_cancr_ap ???? LE);
+qed.
+
+
 lemma exc_opp_x_zero_to_exc_zero_x: 
   ∀G:ogroup.∀x:G.-x ≰ 0 → 0 ≰ x.
 intros (G x H); apply (exc_canc_plusr ??? (-x));
@@ -138,6 +151,13 @@ apply (le_rewl ??? 0 (opp_inverse ??));
 apply (le_rewr ??? x (zero_neutral ??) Px);
 qed.
 
+lemma lt_zero_x_to_lt_opp_x_zero: 
+  ∀G:ogroup.∀x:G.0 < x → -x < 0.
+intros (G x Px); apply (plus_cancr_lt ??? x);
+apply (lt_rewl ??? 0 (opp_inverse ??));
+apply (lt_rewr ??? x (zero_neutral ??) Px);
+qed.
+
 lemma exc_zero_opp_x_to_exc_x_zero: 
   ∀G:ogroup.∀x:G. 0 ≰ -x → x ≰ 0.
 intros (G x H); apply (exc_canc_plusl ??? (-x));
@@ -154,6 +174,15 @@ apply (le_rewl ??? x (zero_neutral ??));
 assumption; 
 qed.
 
+lemma lt_x_zero_to_lt_zero_opp_x: 
+  ∀G:ogroup.∀x:G. x < 0 → 0 < -x.
+intros (G x Lx0); apply (plus_cancr_lt ??? x);
+apply (lt_rewr ??? 0 (opp_inverse ??));
+apply (lt_rewl ??? x (zero_neutral ??));
+assumption; 
+qed.
+
+
 lemma lt0plus_orlt: 
   ∀G:ogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y.
 intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2);