proposition: Theorem reducestar_in_pO : forall (Q : list (poly A0 eqA ltM)) (a : Term A n) (p : list (Term A n)), inPolySet A A0 eqA n ltM p Q -> ~ zeroP (A:=A) A0 eqA (n:=n) a -> reducestar Q (mults (A:=A) multA (n:=n) a p) (pO A n).
proof: Proof. Proof using plusA os cs. intros Q a p H' H'0. cut (canonical A0 eqA ltM p); [ intros Op0 | idtac ]. apply reducestar_eqp_com with (p := mults (A:=A) multA (n:=n) a p) (q := mults (A:=A) multA (n:=n) a (pO A n)); auto. apply reducestar0; auto. apply reduceplus_mults with (1 := cs); auto. apply reduce_imp_reduceplus with (1 := cs); auto. apply reduce_in_pO with (1 := cs); auto. simpl in |- *; apply pO_irreducible; auto. apply inPolySet_imp_canonical with (L := Q); auto. Qed.