proposition: Theorem e_order_eq_pow: exists q, (e_order P_dec w pgroup) = 2 ^ q.
proof: Proof. case (Zdivide_power_2 (e_order P_dec w pgroup) 2 p); auto with zarith. apply Zlt_le_weak; apply e_order_pos. apply prime_2. apply e_order_divide_pow; auto. intros x H; exists x; auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup