proposition: Lemma group_power_0 : forall g : G, Equal (group_power G g (monoid_unit ZZ)) (monoid_unit G).
proof: Proof. unfold group_power in |- *. simpl in |- *. intros g; try assumption. apply Trans with (Z_to_group_nat_fun g 0%Z); auto with algebra. Qed.
imports: Z_group