X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_divisible_group.ma;h=15dd52cdb853ba822b7d35e4a1ab959b0bf6e311;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=a9671d934b082c1bcc3300601108af6c9fce5aee;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/dama/ordered_divisible_group.ma
index a9671d934..15dd52cdb 100644
--- a/helm/software/matita/dama/ordered_divisible_group.ma
+++ b/helm/software/matita/dama/ordered_divisible_group.ma
@@ -35,7 +35,7 @@ coercion cic:/matita/ordered_divisible_group/todg_division.con.
 lemma mul_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x.
 intros (G x n); elim n; simplify; [apply le_reflexive]
 apply (le_transitive ???? H1); 
-apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??));
+apply (Le≪ (0+(n1*x)) (zero_neutral ??));
 apply fle_plusr; assumption;
 qed. 
 
@@ -51,25 +51,25 @@ apply f; assumption;
 qed.
 
 lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
-intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
+intros; elim n; [apply (Lt≫ ? (div1 ??));assumption]
 unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (ltmul_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
-apply (lt_rewl ???? (zero_neutral ??)); 
-apply (lt_rewl ???? (zero_neutral ??)); 
-apply (lt_rewl ???? (mulzero ?n1));
+apply (ltmul_lt ??? (S n1)); simplify; apply (Lt≫ ? f);
+apply (Lt≪ ? (zero_neutral ??)); (* bug se faccio repeat *)
+apply (Lt≪ ? (zero_neutral ??));  
+apply (Lt≪ ? (mulzero ?n1));
 assumption;
 qed.
 
 lemma muleqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
    0<x → 0<y → S n * x ≈ S (n + S m) * y → y < x.
-intros (G x y n m H1 H2 H3); apply (ltmul_lt ??? n); apply (lt_rewr ???? H3);
+intros (G x y n m H1 H2 H3); apply (ltmul_lt ??? n); apply (Lt≫ ? H3);
 clear H3; elim m; [
-  rewrite > sym_plus; simplify; apply (lt_rewl ??? (0+(y+n*y))); [
+  rewrite > sym_plus; simplify; apply (Lt≪ (0+(y+n*y))); [
     apply eq_sym; apply zero_neutral]
   apply flt_plusr; assumption;]
 apply (lt_transitive ???? l); rewrite > sym_plus; simplify;  
 rewrite > (sym_plus n); simplify; repeat apply flt_plusl;
-apply (lt_rewl ???(0+(n1+n)*y)); [apply eq_sym; apply zero_neutral]
+apply (Lt≪ (0+(n1+n)*y)); [apply eq_sym; apply zero_neutral]
 apply flt_plusr; assumption;
 qed.