proposition: Theorem w_in_pgroup: (In w pgroup.(FGroup.s)).
proof: Proof. generalize q_pos; intros HM. generalize q_pos2; intros HM2. assert (H0: 0 < q); auto with zarith. simpl; apply isupport_is_in; auto. assert (zpmult q w (2, q - 1) = (1, 0)). unfold zpmult, w, pmult, base; repeat (rewrite Zmult_1_r || rewrite Zmult_1_l). eq_tac. apply trans_equal with ((3 * q + 1) mod q). eq_tac; auto with zarith. rewrite Zplus_mod; auto. rewrite Zmult_mod; auto. rewrite Z_mod_same; auto with zarith. rewrite Zmult_0_r; repeat rewrite Zmod_small; auto with zarith. apply trans_equal with (2 * q mod q). eq_tac; auto with zarith. apply Zdivide_mod; auto with zarith; exists 2; auto with zarith. apply is_inv_true with (2, q - 1); auto. rewrite zpmult_comm; auto. apply mL_in; auto with zarith. unfold w; apply mL_in; auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup