proposition: Theorem mults_multTerm : forall (p : list (Term A n)) (a b : Term A n), eqP A eqA n (mults (multTerm (A:=A) multA (n:=n) a b) p) (mults a (mults b p)).
proof: Proof. Proof using plusA minusA invA divA cs A1 A0. intros p; elim p; simpl in |- *; auto. intros a l H a0 b; apply (eqpP1 A eqA n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply multTerm_assoc with (1 := cs); auto. Qed.