proposition: Theorem support_in: forall p, 0 <= p < Z_of_nat (length support) -> In (gpow p) support.
proof: Proof. intros p (H, H1); unfold support. rewrite <- (Z.abs_eq p); auto with zarith. rewrite <- (inj_Zabs_nat p); auto. generalize (support_aux_in (Z.abs_nat (g_order G)) 0); simpl; intros H2; apply H2; auto with zarith. rewrite <- (fun x => Zabs_nat_Z_of_nat (@length A x)); auto. apply Zabs_nat_lt; split; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange