proposition: Theorem zpow_w_n: zpow w (2 ^ p) = (1, 0).
proof: Proof. generalize q_pos; intros HM. generalize q_pos2; intros HM2. assert (H0: 0 < q); auto with zarith. replace p with ((p - 1) + 1); auto with zarith. rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. unfold zpow; rewrite gpow_gpow; auto with zarith. generalize zpow_w_n_minus_1; unfold zpow; intros H1; rewrite H1; clear H1. simpl; unfold zpmult, pmult. repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l || rewrite Zplus_0_r || rewrite Zmult_1_r). eq_tac; auto. pattern (-1 mod q) at 1; rewrite <- (Zmod_mod (-1) q); auto with zarith. repeat rewrite <- Zmult_mod; auto. rewrite Zmod_small; auto with zarith. apply w_in_pgroup. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup