proposition: Lemma normalizeK : forall p, to_poly (normalize p) = to_poly p.
proof: Proof. elim => //= a n p <-; case: (normalize p) => //= b m q. case: ifP => //= /eqP ->; case: n => [[]] //= n n0. by rewrite addr0 /cast /cast_pos_nat insubdK /= ?exprD ?mulrA ?addnS. 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)