proposition: Theorem support_not_e: forall b, In b (tail support) -> ~ b = G.(e).
proof: Proof. intros b H; apply (support_aux_not_e (Z.abs_nat (g_order G)) 0); auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange