proposition: Theorem gpow_length_support_is_e: gpow (Z_of_nat (length support)) = G.(e).
proof: Proof. apply (support_aux_length_le_is_e (Z.abs_nat (g_order G)) 0); simpl; auto with zarith. unfold g_order; rewrite Zabs_nat_Z_of_nat; apply ulist_incl_length. rewrite <- (Zabs_nat_Z_of_nat (length G.(s))); auto. exact support_ulist. rewrite <- (Zabs_nat_Z_of_nat (length G.(s))); auto. exact support_incl_G. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange