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