coercion cic:/matita/ordered_divisible_group/todg_division.con.
-lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x.
+lemma mul_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x.
intros (G x n); elim n; simplify; [apply le_reflexive]
apply (le_transitive ???? H1);
apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??));
apply fle_plusr; assumption;
qed.
-lemma lt_ltpow: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y.
+lemma lt_ltmul: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y.
intros; elim n; [simplify; apply flt_plusr; assumption]
simplify; apply (ltplus); [assumption] assumption;
qed.
-lemma ltpow_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y.
+lemma ltmul_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y.
intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption]
simplify in l; cases (ltplus_orlt ????? l); [assumption]
apply f; assumption;
lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (ltpow_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
+apply (ltmul_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
apply (lt_rewl ???? (zero_neutral ??));
apply (lt_rewl ???? (zero_neutral ??));
-apply (lt_rewl ???? (powzero ?n1));
+apply (lt_rewl ???? (mulzero ?n1));
assumption;
qed.
-lemma poweqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
+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 (ltpow_lt ??? n); apply (lt_rewr ???? H3);
+intros (G x y n m H1 H2 H3); apply (ltmul_lt ??? n); apply (lt_rewr ???? H3);
clear H3; elim m; [
rewrite > sym_plus; simplify; apply (lt_rewl ??? (0+(y+n*y))); [
apply eq_sym; apply zero_neutral]