proposition: Lemma to_hpolyK : cancel to_hpoly to_poly.
proof: Proof. elim/poly_ind; rewrite /to_hpoly ?polyseq0 // => p c ih. rewrite -{1}cons_poly_def polyseq_cons. have [|pn0] /= := nilP. rewrite -polyseq0 => /poly_inj ->; rewrite mul0r add0r. apply/poly_inj; rewrite !polyseqC. by case c0: (c == 0); rewrite ?polyseq0 // polyseqC c0. by case: (polyseq p) ih => /= [<-| a l -> //]; rewrite mul0r add0r. 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)