proposition: Theorem reduce_in_pO : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), inPolySet p Q -> reduce Q p (pO A n).
proof: Proof. Proof using plusA os cs. intros Q p; case p; simpl in |- *; auto. intros H'; elim (inPolySet_is_pX (pO A n) Q); [ intros a E; elim E; intros q E0; inversion E0 | idtac ]; auto. intros a l H'. cut (canonical A0 eqA ltM (pX a l)); [ intros Op0 | idtac ]. cut (canonical A0 eqA ltM l); [ intros Op1 | apply canonical_imp_canonical with (a := a) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ intros Nza | idtac ]. cut (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a a Nza l l = pO A n). intros H'0; rewrite <- H'0. change (reduce Q (pX a l) (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a a Nza l l)) in |- *. apply reducetop with (b := a) (nZb := Nza) (q := l); auto. apply divP_on_eqT with (1 := cs); auto. cut (eqP A eqA n (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a a Nza l l) (pO A n)). intros H'0; inversion H'0; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec l (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=a) Nza) l)); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec l (mults (A:=A) multA (n:=n) (T1 A1 n) l)); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec l l); auto. apply minuspf_refl with (1 := cs); auto. apply (canonical_nzeroP A A0 eqA n ltM) with (p := l); auto. apply inPolySet_imp_canonical with (L := Q); auto. Qed.