-alias num (instance 0) = "natural number".
-axiom core1: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.
+lemma muleqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
+ 0<x → 0<y → S n * x ≈ S (n + S m) * y → y < x.
+intros (G x y n m H1 H2 H3); apply (ltmul_lt ??? n); apply (Lt≫ ? H3);
+clear H3; elim m; [
+ rewrite > sym_plus; simplify; apply (Lt≪ (0+(y+n*y))); [
+ apply eq_sym; apply zero_neutral]
+ apply flt_plusr; assumption;]
+apply (lt_transitive ???? l); rewrite > sym_plus; simplify;
+rewrite > (sym_plus n); simplify; repeat apply flt_plusl;
+apply (Lt≪ (0+(n1+n)*y)); [apply eq_sym; apply zero_neutral]
+apply flt_plusr; assumption;
+qed.
+