proposition: Lemma group_power_S : forall (g : G) (n : ZZ), Equal (group_power G g (sgroup_law ZZ n (ring_unit ZZ))) (sgroup_law G (group_power G g n) g).
proof: Proof. unfold group_power in |- *. simpl in |- *. intros g n; try assumption. apply Trans with (sgroup_law G (Z_to_group_fun g n) (Z_to_group_fun g (ring_unit Zr))); auto with algebra. Qed.
imports: Z_group