proposition: Lemma sgroup_powers_prop : forall (G : GROUP) (g x : G), in_part x (sgroup_powers g) -> exists n : ZZ, Equal x (group_power G g n).
proof: Proof. intros G g x H'; try assumption. elim H'. intros x0 H'0; try assumption. elim H'0; intros H'1 H'2; try exact H'2; clear H'0. exists x0; try assumption. Qed.
imports: Zring Group_kernel