proposition: Theorem pmult_comm: forall p q, (pmult p q) = (pmult q p).
proof: Proof. intros p q; case p; case q; intros q1 q2 p1 p2; unfold pmult. eq_tac; ring. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup