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