proposition: Lemma sgroup_powers_rev : forall (G : GROUP) (g : G) (n : ZZ), in_part (group_power G g n) (sgroup_powers g).
proof: Proof. intros G g n; try assumption. simpl in |- *. exists n; split; [ idtac | try assumption ]. auto with *. unfold group_power in |- *; auto with *. Qed.
imports: Zring Group_kernel