proposition: Lemma minPoly_XsubC : reflect (minPoly K x = 'X - x%:P) (x \in K).
proof: Proof. set p := minPoly K x; apply: (iffP idP) => [Kx | Dp]; last first. suffices ->: x = - p`_0 by rewrite rpredN (polyOverP minPolyOver). by rewrite Dp coefB coefX coefC add0r opprK. rewrite (@all_roots_prod_XsubC _ p [:: x]) /= ?root_minPoly //. by rewrite big_seq1 (monicP (monic_minPoly K x)) scale1r. by apply/eqP; rewrite size_minPoly eqSS adjoin_deg_eq1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)