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