proposition: Theorem multpf_smultm_assoc : forall (p q : list (Term A n)) (a : Term A n), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> ~ zeroP (A:=A) A0 eqA (n:=n) a -> eqP A eqA n (mults (A:=A) multA (n:=n) a (multpf p q)) (multpf (mults (A:=A) multA (n:=n) a p) q).
proof: Proof. Proof using os minusA invA divA cs A1. intros p q a; elim p; simpl in |- *; auto. intros a0 l H' H'0 H'1 H'2. cut (~ zeroP (A:=A) A0 eqA (n:=n) a0); [ intros nZ0 | apply canonical_nzeroP with (ltM := ltM) (p := l) ]; auto. cut (canonical A0 eqA ltM l); [ intros Op0 | apply canonical_imp_canonical with (a := a0) ]; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a (mults (A:=A) multA (n:=n) a0 q)) (mults (A:=A) multA (n:=n) a (multpf l q))); auto. apply eqp_pluspf_com with (1 := cs); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.