proposition: Theorem e_order_le_pow : e_order P_dec w pgroup <= 2 ^ p.
proof: Proof. apply Zdivide_le. apply Zlt_le_weak; apply e_order_pos. apply Zpower_gt_0; auto with zarith. apply e_order_divide_pow. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup