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