proposition: Theorem zpow_def: forall a b, In a pgroup.(FGroup.s) -> 0 <= b -> zpow a b = ((fst (ppow a b)) mod q, (snd (ppow a b)) mod q).
proof: Proof. generalize q_pos; intros HM. generalize q_pos2; intros HM2. assert (H0: 0 < q); auto with zarith. intros a b Ha Hb; generalize Hb; pattern b; apply natlike_ind; auto. intros _; repeat rewrite Zmod_small; [auto with zarith..|]. rewrite ppow_0; simpl; auto with zarith. unfold zpow; intros n1 H Rec _; unfold Z.succ. rewrite gpow_add; auto with zarith. rewrite ppow_add; simpl; try rewrite pmult_1_r; auto with zarith. rewrite Rec; unfold zpmult; auto with zarith. case (ppow a n1); case a; unfold pmult, fst, snd. intros x y z t. repeat (rewrite Zmult_1_r || rewrite Zmult_0_r || rewrite Zplus_0_r || rewrite Zplus_0_l); eq_tac. repeat rewrite (fun u v => Zplus_mod (u * v)); auto. eq_tac; try eq_tac; auto. repeat rewrite (Zmult_mod z); auto with zarith. repeat rewrite (fun u v => Zmult_mod (u * v)); auto. eq_tac; try eq_tac; auto with zarith. repeat rewrite (Zmult_mod base); auto with zarith. eq_tac; try eq_tac; auto with zarith. apply Zmod_mod; auto. apply Zmod_mod; auto. repeat rewrite (fun u v => Zplus_mod (u * v)); auto. eq_tac; try eq_tac; auto. repeat rewrite (Zmult_mod z); auto with zarith. repeat rewrite (Zmult_mod t); auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup