include "ordered_sets.ma".
record pre_ordered_abelian_group : Type ≝
- { og_abelian_group:> abelian_group;
- og_tordered_set_: tordered_set;
- og_with: exc_carr og_tordered_set_ = og_abelian_group
+ { og_abelian_group_: abelian_group;
+ og_tordered_set:> tordered_set;
+ og_with: carr og_abelian_group_ = og_tordered_set
}.
-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]
qed.
-coercion cic:/matita/ordered_groups/og_tordered_set.con.
+coercion cic:/matita/ordered_groups/og_abelian_group.con.
definition is_ordered_abelian_group ≝
λG:pre_ordered_abelian_group. ∀f,g,h:G. f≤g → f+h≤g+h.