proposition: Theorem mults_comp : forall (a b : Term A n) (p q : list (Term A n)), eqTerm (A:=A) eqA (n:=n) a b -> eqP A eqA n p q -> eqP A eqA n (mults a p) (mults b q).
proof: Proof. Proof using plusA minusA invA divA cs A1 A0. intros a b p q H' H'0; elim H'0; simpl in |- *; auto. Qed.