proposition: Lemma elim_poly : forall p, exists p' c, p = p' * 'X + c%:P.
proof: Proof. elim/poly_ind; first by exists 0, 0; rewrite mul0r add0r. by move=> p c [_ [_]] _; exists p, c. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)