proposition: Theorem e_order_divide_order: (e_order P_dec w pgroup | g_order pgroup).
proof: Proof. apply e_order_divide_g_order. apply w_in_pgroup. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup