+lemma le_rewl: ∀E:excedence.∀x,z,y:E. x ≈ y → x ≤ z → y ≤ z.
+intros (E x z y); apply (le_transitive ???? ? H1);
+clear H1 z; unfold in H; unfold; intro H1; apply H; clear H;
+lapply ap_cotransitive;
+intros (G x z y); intro Eyz;
+
+
+lemma plus_cancr_le:
+ ∀G:ordered_abelian_group.∀x,y,z:G.x+z ≤ y + z → x ≤ y.
+intros 5 (G x y z L);
+
+ apply L; clear L; elim (exc_cotransitive ???z Exy);
+