proposition: Lemma group_power_1 : forall g : G, Equal (group_power G g (ring_unit ZZ)) g.
proof: Proof. intros g; try assumption. apply Trans with (group_power G g (sgroup_law ZZ (monoid_unit ZZ) (ring_unit ZZ))); auto with algebra. Qed.
imports: Z_group