proposition: Lemma pO_reducestar : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), reducestar Q (pO A n) p -> p = pO A n.
proof: Proof. intros Q p H'. cut (reduceplus A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (pO A n) p); [ intros Red1 | apply reducestar_reduceplus; auto ]. apply pO_reduceplus with (2 := Red1); auto. Qed.