+
+lemma appow_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 pluspow: ∀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 powzero: ∀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.
+