X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_group.ma;h=44529cadf4d9a185e3810b1ffd7c53455b649e47;hb=7abdf2f1764ba67a48f0829f7a9813ce7426b0c6;hp=8677e755ba6902a649cf990ffcaaceb7332caea4;hpb=46fb7c601185d7aada2489700e7d7817d50e1e57;p=helm.git

diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 8677e755b..44529cadf 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -19,14 +19,14 @@ include "group.ma".
 record pogroup_ : Type ≝ { 
   og_abelian_group_: abelian_group;
   og_excess:> excess;
-  og_with: carr og_abelian_group_ = apart_of_excess og_excess
+  og_with: carr og_abelian_group_ = exc_ap og_excess
 }.
 
 lemma og_abelian_group: pogroup_ → abelian_group.
-intro G; apply (mk_abelian_group G); [1,2,3: rewrite < (og_with G)]
-[apply (plus (og_abelian_group_ G));|apply zero;|apply opp]
-unfold apartness_OF_pogroup_; cases (og_with G); simplify;
-[apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
+intro G; apply (mk_abelian_group G); unfold apartness_OF_pogroup_;
+cases (og_with G); simplify;
+[apply (plus (og_abelian_group_ G));|apply zero;|apply opp
+|apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
 qed.
 
 coercion cic:/matita/ordered_group/og_abelian_group.con.