proposition: Theorem tmults_zerop_eqp_pO : forall p a, zeroP (A:=A) A0 eqA (n:=n) a -> eqP A eqA n (tmults a p) (pO A n).
proof: Proof. intros p a; unfold tmults in |- *; case (zeroP_dec A A0 eqA eqA_dec n a); auto. intros H' H'0; elim H'; auto. Qed.