proposition: Theorem gpow_in: forall n, In (gpow n) G.(s).
proof: Proof. intros n; case n; simpl; auto. intros p; apply iter_pos_invariant with (Inv := fun x => In x G.(s)); auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange