proposition: Theorem reduce_mults : forall (Q : list (poly A0 eqA ltM)) (a : Term A n) (p q : list (Term A n)), reduce Q p q -> canonical A0 eqA ltM p -> ~ zeroP (A:=A) A0 eqA (n:=n) a -> reduce Q (mults (A:=A) multA (n:=n) a p) (mults (A:=A) multA (n:=n) a q).
proof: Proof. Proof using plusA os cs. intros Q a p q H'; generalize a; elim H'; clear a H'; auto. simpl in |- *; auto. intros a b nZb p0 q0 r H' H'0 H'1 a0 H'2 H'3. cut (~ zeroP (A:=A) A0 eqA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a)); [ intros nZ0 | idtac ]; auto. apply reducetop with (b := b) (nZb := nZb) (q := q0); auto. apply divTerm_def with (nZb := nZb); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (multTerm (A:=A) multA (n:=n) a0 (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=b) nZb)) b); [ auto | idtac ]. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) a0 (multTerm (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=b) nZb) b)); [ auto | idtac ]. apply multTerm_assoc with (1 := cs); auto. apply eqTerm_multTerm_comp with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply divTerm_multTerm_l with (1 := cs); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) a0 (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b nZb p0 q0)); auto. apply spminusf_multTerm with (1 := cs); auto. apply canonical_imp_canonical with (a := a); auto. apply canonical_imp_canonical with (a := b); auto. apply inPolySet_imp_canonical with (L := Q); auto. apply nzeroP_multTerm with (1 := cs); auto. apply canonical_nzeroP with (ltM := ltM) (p := p0); auto. intros a b p0 q0 H' H'0 H'1 a0 H'2 H'3. simpl in |- *; apply reduceskip; auto. apply H'0; auto. apply canonical_imp_canonical with (a := a); auto. Qed.