proposition: Theorem e_order_divide_pow: (e_order P_dec w pgroup | 2 ^ p).
proof: Proof. generalize q_pos; intros HM. generalize q_pos2; intros HM2. assert (H0: 0 < q); auto with zarith. apply e_order_divide_gpow. apply w_in_pgroup. apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. exact zpow_w_n. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup