proposition: Theorem spminusf_multTerm : forall (a b c : Term A n) (nZc : ~ zeroP (A:=A) A0 eqA (n:=n) c) (p q : list (Term A n)), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> divP A A0 eqA multA divA n b c -> ~ zeroP (A:=A) A0 eqA (n:=n) a -> eqP A eqA n (spminusf (multTerm (A:=A) multA (n:=n) a b) c nZc (mults (A:=A) multA (n:=n) a p) q) (mults (A:=A) multA (n:=n) a (spminusf b c nZc p q)).
proof: Proof. Proof using plusA os cs. intros a b c nZc p q H' H'0 H'1 H'2; unfold spminusf in |- *. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (mults (A:=A) multA (n:=n) a p) (mults (A:=A) multA (n:=n) (multTerm (A:=A) multA (n:=n) a (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) b (b:=c) nZc)) q)); [ auto | idtac ]. apply minuspf_comp with (1 := cs); auto. apply canonical_mults with (1 := cs); auto. apply nzeroP_comp_eqTerm with (1 := cs) (a := multTerm (A:=A) multA (n:=n) a (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) b (b:=c) nZc)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply divTerm_multTerm_l with (1 := cs). inversion H'1; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (mults (A:=A) multA (n:=n) a p) (mults (A:=A) multA (n:=n) a (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) b (b:=c) nZc) q))); [ auto | idtac ]. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply mults_dist_minuspf with (1 := cs); auto. Qed.