+lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group.
+ intro F;
+ apply mk_ordered_abelian_group;
+ [ apply mk_pre_ordered_abelian_group;
+ [ apply (r_abelian_group F)
+ | apply (og_ordered_set (of_ordered_abelian_group_ F))
+ | apply (eq_f ? ? carrier);
+ apply (of_with2 F)
+ ]
+ |
+ apply
+ (eq_rect' ? ?
+ (λG:abelian_group.λH:og_abelian_group (of_ordered_abelian_group_ F)=G.
+ is_ordered_abelian_group
+ (mk_pre_ordered_abelian_group G (of_ordered_abelian_group_ F)
+ (eq_f abelian_group Type carrier (of_ordered_abelian_group_ F) G
+ H)))
+ ? ? (of_with2 F));
+ simplify;
+ apply (og_ordered_abelian_group_properties (of_ordered_abelian_group_ F))
+ ]
+qed.
+
+coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con.
+
+(*CSC: I am not able to prove this since unfold is undone by coercion composition*)
+axiom of_with1:
+ ∀G:pre_ordered_field_ch0.
+ cos_ordered_set (of_cotransitively_ordered_set_ G) =
+ og_ordered_set (of_ordered_abelian_group G).
+