proposition: Lemma RhpolyE p q : refines Rhpoly p q -> p = to_poly q.
proof: Proof. by rewrite refinesE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements pos hrel poly_op)