proposition: Theorem mults_eqp_inv : forall (a : Term A n) (p q : list (Term A n)), eqP A eqA n (mults (A:=A) multA (n:=n) a p) (mults (A:=A) multA (n:=n) a q) -> ~ zeroP (A:=A) A0 eqA (n:=n) a -> eqP A eqA n p q.
proof: Proof. Proof using plusA minusA invA divA cs A1. intros a p; elim p; auto. intros q; case q; simpl in |- *; auto. intros t l H'; inversion_clear H'; auto. intros a0 l H' q; case q; simpl in |- *; auto. intros H'0; inversion_clear H'0; auto. intros t l0 H'0; inversion_clear H'0; auto. intros H'1. change (eqP A eqA n (pX a0 l) (pX t l0)) in |- *. apply eqpP1; auto. apply multTerm_eqTerm_inv with (1 := cs) (a := a); auto. Qed.