-lemma pippo4: ∀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);
-cases (pippo2 ????? Hletin); [left|right] apply tog_total; assumption;
+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_excess ??? H1);
+cases (excplus_orexc ????? Hletin); [left|right] apply tog_total; assumption;
+qed.
+
+lemma excplus: ∀G:togroup.∀a,b,c,d:G.a ≰ b → c ≰ d → a + c ≰ b + d.
+intros (G a b c d L1 L2);
+lapply (fexc_plusr ??? (c) L1) as L3;
+elim (exc_cotransitive ??? (b+d) L3); [assumption]
+lapply (plus_cancl_exc ???? t); lapply (tog_total ??? Hletin);
+cases Hletin1; cases (H L2);