let rec gpow (G : abelian_group) (x : G) (n : nat) on n : G ≝
match n with [ O ⇒ 0 | S m ⇒ x + gpow ? x m].
-interpretation "additive abelian group pow" 'times n x =
- (cic:/matita/divisible_group/gpow.con _ x n).
+interpretation "additive abelian group pow" 'times n x = (gpow _ x n).
record dgroup : Type ≝ {
dg_carr:> abelian_group;
intros (G x n); cases (dg_prop G x n); apply w;
qed.
-interpretation "divisible group divide" 'divide x n =
- (cic:/matita/divisible_group/divide.con _ x n).
+interpretation "divisible group divide" 'divide x n = (divide _ x n).
lemma divide_divides:
∀G:dgroup.∀x:G.∀n. S n * (x / n) ≈ x.