proposition: Theorem pmult_comm: forall p q, pmult p q = pmult q p.
proof: Proof. intros p q; unfold pmult; rewrite Zmult_comm; auto. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression