-lemma og_tordered_set: pre_ordered_abelian_group → tordered_set.
-intro G; apply mk_tordered_set;
-[1: apply mk_pordered_set;
- [1: apply (mk_excedence G);
- [1: cases G; clear G; simplify; rewrite < H; clear H;
- cases og_tordered_set_; clear og_tordered_set_; simplify;
- cases tos_poset; simplify; cases pos_carr; simplify; assumption;
- |2: cases G; simplify; cases H; simplify; clear H;
- cases og_tordered_set_; simplify; clear og_tordered_set_;
- cases tos_poset; simplify; cases pos_carr; simplify;
- intros; apply H;
- |3: cases G; simplify; cases H; simplify; cases og_tordered_set_; simplify;
- cases tos_poset; simplify; cases pos_carr; simplify;
- intros; apply c; assumption]
- |2: cases G; simplify;
- cases H; simplify; clear H; cases og_tordered_set_; simplify;
- cases tos_poset; simplify; assumption;]
-|2: simplify; (* SLOW, senza la simplify il widget muore *)
- cases G; simplify;
- generalize in match (tos_totality og_tordered_set_);
- unfold total_order_property;
- cases H; simplify; cases og_tordered_set_; simplify;
- cases tos_poset; simplify; cases pos_carr; simplify;
- intros; apply f; assumption;]
+lemma og_abelian_group: pre_ordered_abelian_group → 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_pre_ordered_abelian_group; cases (og_with G); simplify;
+[apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]