proposition: Theorem mults_eqp_zpO : forall a : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> forall p : list (Term A n), eqP A eqA n (mults a p) (pO A n) -> eqP A eqA n p (pO A n).
proof: Proof. intros a H' p; elim p; simpl in |- *; auto. intros a0 l H'0 H'1; inversion H'1; auto. Qed.