(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/ordered_group/".
+
include "group.ma".
record pogroup_ : Type ≝ {
og_abelian_group_: abelian_group;
- og_excedence:> excedence;
- og_with: carr og_abelian_group_ = apart_of_excedence og_excedence
+ og_excess:> excess;
+ og_with: carr og_abelian_group_ = apart_of_excess og_excess
}.
lemma og_abelian_group: pogroup_ → abelian_group.
assumption;
qed.
+lemma lt_opp_x_zero_to_lt_zero_x:
+ ∀G:pogroup.∀x:G. -x < 0 → 0 < x.
+intros (G x Lx0); apply (plus_cancr_lt ??? (-x));
+apply (lt_rewl ??? (-x) (zero_neutral ??));
+apply (lt_rewr ??? (-x+x) (plus_comm ???));
+apply (lt_rewr ??? 0 (opp_inverse ??));
+assumption;
+qed.
lemma lt0plus_orlt:
∀G:pogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y.
lemma lexxyy_lexy: ∀G:togroup. ∀x,y:G. x+x ≤ y+y → x ≤ y.
intros (G x y H); intro H1; lapply (tog_total ??? H1) as H2;
-lapply (ltxy_ltyyxx ??? H2) as H3; lapply (lt_to_excede ??? H3) as H4;
+lapply (ltxy_ltyyxx ??? H2) as H3; lapply (lt_to_excess ??? H3) as H4;
cases (H H4);
qed.
qed.
lemma leplus_lt_le: ∀G:togroup.∀x,y:G. 0 ≤ x + y → x < 0 → 0 ≤ y.
-intros; intro; apply H; lapply (lt_to_excede ??? l);
+intros; intro; apply H; lapply (lt_to_excess ??? l);
lapply (tog_total ??? e);
lapply (tog_total ??? Hletin);
lapply (ltplus ????? Hletin2 Hletin1);
apply (exc_rewl ??? (0+0)); [apply eq_sym; apply zero_neutral]
-apply lt_to_excede; assumption;
+apply lt_to_excess; assumption;
qed.
lemma ltplus_orlt: ∀G:togroup.∀a,b,c,d:G. a+c < b + d → a < b ∨ c < d.
-intros (G a b c d H1 H2); lapply (lt_to_excede ??? H1);
+intros (G a b c d H1 H2); lapply (lt_to_excess ??? H1);
cases (excplus_orexc ????? Hletin); [left|right] apply tog_total; assumption;
qed.