+apply (Ap≪ ? (plus_comm ???));
+apply (Ap≪ w (zero_neutral ??)); assumption;
+qed.
+
+lemma apmul_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y.
+intros 4 (G x y n); elim n; [2:
+ simplify in a;
+ cases (applus ????? a); [assumption]
+ apply f; assumption;]
+apply (plus_cancr_ap ??? 0); assumption;
+qed.
+
+lemma plusmul: ∀G:dgroup.∀x,y:G.∀n.n * (x+y) ≈ n * x + n * y.
+intros (G x y n); elim n; [
+ simplify; apply (Eq≈ 0 ? (zero_neutral ? 0)); apply eq_reflexive]
+simplify; apply eq_sym; apply (Eq≈ (x+y+(n1*x+n1*y))); [
+ apply (Eq≈ (x+(n1*x+(y+(n1*y))))); [
+ apply eq_sym; apply plus_assoc;]
+ apply (Eq≈ (x+((n1*x+y+(n1*y))))); [
+ apply feq_plusl; apply plus_assoc;]
+ apply (Eq≈ (x+(y+n1*x+n1*y))); [
+ apply feq_plusl; apply feq_plusr; apply plus_comm;]
+ apply (Eq≈ (x+(y+(n1*x+n1*y)))); [
+ apply feq_plusl; apply eq_sym; apply plus_assoc;]
+ apply plus_assoc;]
+apply feq_plusl; apply eq_sym; assumption;
+qed.
+
+lemma mulzero: ∀G:dgroup.∀n.n*0 ≈ 0. [2: apply dg_carr; apply G]
+intros; elim n; [simplify; apply eq_reflexive]
+simplify; apply (Eq≈ ? (zero_neutral ??)); assumption;
+qed.
+
+let rec gpowS (G : abelian_group) (x : G) (n : nat) on n : G ≝
+ match n with [ O ⇒ x | S m ⇒ gpowS ? x m + x].
+
+lemma gpowS_gpow: ∀G:dgroup.∀e:G.∀n. S n * e ≈ gpowS ? e n.
+intros (G e n); elim n; simplify; [
+ apply (Eq≈ ? (plus_comm ???));apply zero_neutral]
+apply (Eq≈ ?? (plus_comm ???));
+apply (Eq≈ (e+S n1*e) ? H); clear H; simplify; apply eq_reflexive;
+qed.
+
+lemma divpow: ∀G:dgroup.∀e:G.∀n. e ≈ gpowS ? (e/n) n.
+intros (G e n); apply (Eq≈ ?? (gpowS_gpow ?(e/n) n));
+apply eq_sym; apply divide_divides;