proposition: Theorem zpow_w_n_minus_1: zpow w (2 ^ (p - 1)) = (-1 mod q, 0).
proof: Proof. generalize q_pos; intros HM. generalize q_pos2; intros HM2. assert (H0: 0 < q); auto with zarith. rewrite zpow_def. replace (p - 1) with ((p - 2) + 1); auto with zarith. rewrite sn_w; auto with zarith. generalize Mp_divide_sn (sn_snd (p - 2)); case (s (p -2)); case (ppow w (2 ^ (p -2))). unfold fst, snd; intros x y z t H1 H2; unfold pmult, pplus; subst. repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l || rewrite Zplus_0_r). assert (H2: z mod q = 0). case H1; intros q1 Hq1; rewrite Hq1. case q_divide_Mp; intros q2 Hq2; rewrite Hq2. rewrite Zmult_mod; auto. rewrite (Zmult_mod q2); auto. rewrite Z_mod_same; auto with zarith. repeat (rewrite Zmult_0_r; rewrite (Zmod_small 0)); auto with zarith. assert (H3: forall x, (z * x) mod q = 0). intros y1; rewrite Zmult_mod; try rewrite H2; auto. assert (H4: forall x y, (z * x + y) mod q = y mod q). intros x1 y1; rewrite Zplus_mod; try rewrite H3; auto. rewrite Zplus_0_l; apply Zmod_mod; auto. eq_tac; auto. apply w_in_pgroup. apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup