proposition: Theorem pmult_assoc: forall p q r, (pmult p (pmult q r)) = (pmult (pmult p q) r).
proof: Proof. assert (Hu: 0 < n); try apply Z.lt_trans with 1; auto with zarith. generalize Zmod_mod; intros H. intros p q r; unfold pmult. rewrite (Zmult_mod p); auto. repeat rewrite Zmod_mod; auto. rewrite (Zmult_mod q); auto. rewrite <- Zmult_mod; auto. rewrite Zmult_assoc. rewrite (Zmult_mod (p * (q mod n))); auto. rewrite (Zmult_mod ((p * q) mod n)); auto. eq_tac; auto. eq_tac; auto. rewrite (Zmult_mod p); sauto. rewrite Zmod_mod; auto. rewrite <- Zmult_mod; sauto. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression