proposition: Theorem support_incl_G: incl support G.(s).
proof: Proof. intros a1 H; case (support_gpow a1); auto; intros p (H1, H2); subst; apply gpow_in. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange