proposition: Theorem CombLinear_mults1 : forall (Q : list (poly A0 eqA ltM)) (a : Term A n) (p : list (Term A n)), ~ zeroP (A:=A) A0 eqA (n:=n) a -> CombLinear Q p -> CombLinear Q (mults (A:=A) multA (n:=n) a p).
proof: Proof. Proof using os minusA invA divA cs A1. intros Q a p H' H'0; elim H'0; auto. intros a0 p0 q s H'1 H'2 H'3 H'4 H'5. cut (canonical A0 eqA ltM q); [ intros C0 | apply inPolySet_imp_canonical with (L := Q); auto ]. cut (canonical A0 eqA ltM p0); [ intros Op1 | apply CombLinear_canonical with (Q := Q); auto ]. apply CombLinear_1 with (a := multTerm (A:=A) multA (n:=n) a a0) (p := mults (A:=A) multA (n:=n) a p0) (q := q); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) a (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a0 q) p0)); 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 p0)); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.