fact: Definition selectpolyf : forall (Q : list (poly A0 eqA ltM)) (r : list (Term A n)), canonical A0 eqA ltM r -> {q : list (Term A n) | reduce A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q r q} + {irreducible A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q r}.