+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.
+
+