proposition: Theorem e_order_divide_g_order: (e_order | g_order G).
proof: Proof. change ((g_order Gsupport) | g_order G). apply lagrange; auto. exact support_incl_G. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange