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.