proposition: Theorem gpow_support_not_e: forall p, 0 < p < Z_of_nat (length support) -> gpow p <> G.(e).
proof: Proof. intros p (H1, H2); apply gpow_support_aux_not_e with (m := 0) (n := length G.(s)); simpl; try split; auto with zarith. rewrite <- (Zabs_nat_Z_of_nat (length G.(s))); auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange