An unimplemented case of clearbody is now implemented.

[helm.git] / helm / software / matita / dama / ordered_group.ma

diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 8677e755ba6902a649cf990ffcaaceb7332caea4..44529cadf4d9a185e3810b1ffd7c53455b649e47 100644 (file)
--- 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.