proposition: Theorem in_minuspf_spoly_in : forall a b : Term A n, eqT (ppc (A:=A) A1 (n:=n) a b) (multTerm (A:=A) multA (n:=n) a b) -> forall p q : list (Term A n), canonical A0 eqA ltM (pX a p) -> canonical A0 eqA ltM (pX b q) -> forall c : Term A n, In c (mults (A:=A) multA (n:=n) b p) -> In c (minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (mults (A:=A) multA (n:=n) b p) (mults (A:=A) multA (n:=n) a q)).
proof: Proof. Proof using plusA os divA cs. intros a b H' p q H'0 H'1 c H'2. cut (canonical A0 eqA ltM p); [ intros Op0 | apply canonical_imp_canonical with (a := a) ]; auto. cut (canonical A0 eqA ltM q); [ intros Op1 | apply canonical_imp_canonical with (a := b) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ intros Z0 | apply canonical_nzeroP with (ltM := ltM) (p := p) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) b); [ intros Z1 | apply canonical_nzeroP with (ltM := ltM) (p := q) ]; auto. apply minuspf_spoly_in with (a := a) (b := b) (nZa := Z0) (nZb := Z1); auto. intros c0 H'6. apply multTerm_or_z_d1 with (p := p); auto. intros c0 H'6. apply multTerm_or_z_d2 with (p := q); auto. Qed.