proposition: Theorem mults_com : 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 (multTerm (A:=A) multA (n:=n) b a) p).
proof: Proof. Proof using plusA minusA invA divA cs A1 A0. intros p; elim p; simpl in |- *; auto. Qed.