proposition: Theorem e_order_eq_p: e_order P_dec w pgroup = 2 ^ p.
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 p1 Hp1. case (Zle_lt_or_eq p1 p); try (intro H1; subst; auto; fail). case (Zle_or_lt p1 p); auto; intros H1. absurd (2 ^ p1 <= 2 ^ p); auto with zarith. apply Zlt_not_le; apply Zpower_lt_monotone; auto with zarith. apply Zdivide_le. apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. apply Zpower_gt_0; auto with zarith. rewrite <- Hp1; apply e_order_divide_pow. intros H1. assert (Hu: 0 <= p1). generalize Hp1; case p1; simpl; auto with zarith. intros p2 Hu; absurd (0 < e_order P_dec w pgroup). rewrite Hu; auto with zarith. apply e_order_pos. absurd (zpow w (2 ^ (p - 1)) = (1, 0)). rewrite zpow_w_n_minus_1. intros H2; injection H2; clear H2; intros H2. assert (H0: 0 < q); auto with zarith. absurd (0 mod q = 0). pattern 0 at 1; replace 0 with (-1 + 1); auto with zarith. rewrite Zplus_mod; auto with zarith. rewrite H2; rewrite (Zmod_small 1); auto with zarith. rewrite Zmod_small; auto with zarith. rewrite Zmod_small; auto with zarith. unfold zpow; apply (gpow_pow _ _ w pgroup) with p1; auto with zarith. apply w_in_pgroup. rewrite <- Hp1. apply (gpow_e_order_is_e _ P_dec _ w pgroup). apply w_in_pgroup. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup