apply (fle_plusl ??? (-z) L);
qed.
+lemma plus_cancl_lt:
+ ∀G:ogroup.∀x,y,z:G.z+x < z+y → x < y.
+intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancl_le; assumption]
+apply (plus_cancl_ap ???? LE);
+qed.
+
+lemma plus_cancr_lt:
+ ∀G:ogroup.∀x,y,z:G.x+z < y+z → x < y.
+intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancr_le; assumption]
+apply (plus_cancr_ap ???? LE);
+qed.
+
+
lemma exc_opp_x_zero_to_exc_zero_x:
∀G:ogroup.∀x:G.-x ≰ 0 → 0 ≰ x.
intros (G x H); apply (exc_canc_plusr ??? (-x));
apply (le_rewr ??? x (zero_neutral ??) Px);
qed.
+lemma lt_zero_x_to_lt_opp_x_zero:
+ ∀G:ogroup.∀x:G.0 < x → -x < 0.
+intros (G x Px); apply (plus_cancr_lt ??? x);
+apply (lt_rewl ??? 0 (opp_inverse ??));
+apply (lt_rewr ??? x (zero_neutral ??) Px);
+qed.
+
lemma exc_zero_opp_x_to_exc_x_zero:
∀G:ogroup.∀x:G. 0 ≰ -x → x ≰ 0.
intros (G x H); apply (exc_canc_plusl ??? (-x));
assumption;
qed.
+lemma lt_x_zero_to_lt_zero_opp_x:
+ ∀G:ogroup.∀x:G. x < 0 → 0 < -x.
+intros (G x Lx0); apply (plus_cancr_lt ??? x);
+apply (lt_rewr ??? 0 (opp_inverse ??));
+apply (lt_rewl ??? x (zero_neutral ??));
+assumption;
+qed.
+
+
lemma lt0plus_orlt:
∀G:ogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y.
intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2);