proposition: Theorem support_gpow: forall b, (In b support) -> exists p, 0 <= p < Z_of_nat (length support) /\ b = gpow p.
proof: Proof. intros b H; case (support_aux_gpow (Z.abs_nat (g_order G)) 0 b); auto with zarith. intros p ((H1, H2), H3); exists (Z_of_nat p); repeat split; auto with zarith. apply inj_lt; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange