proposition: Lemma comp_mxminpolyK : forall (p : {poly F}), p \is monic -> (1 < size p)%N -> mxminpoly (companion_mx p) = p.
proof: Proof. move=> p Hp Hs. set A := companion_mx p. suff Hn: forall q, horner_mx A q = 0 -> (q == 0) || ((size p).-2 < (size q).-1)%N. have Hm0: (mxminpoly A == 0) = false. by apply: negbTE; rewrite monic_neq0 // mxminpoly_monic. have:= Hn (mxminpoly A) (mx_root_minpoly A); rewrite Hm0 /= => Hmn. have Hsm : size (mxminpoly A) == size (char_poly A). rewrite eqn_leq dvdp_leq ?mxminpoly_dvd_char ?monic_neq0 ?char_poly_monic //. by rewrite size_char_poly -(addn1 _.-2) addnC -ltn_subRL subn1. apply/eqP; rewrite -eqp_monic // ?mxminpoly_monic //. by rewrite -{2}(comp_char_polyK Hp) // -dvdp_size_eqp // mxminpoly_dvd_char. move=> q; case: (ltnP (size p).-2 (size q).-1); first by rewrite orbT. have H (i : 'I_(size p).-2): A *m col (widen_ord (leqnSn (size p).-2) i) 1%:M = col (lift ord0 i) 1%:M. rewrite col_id_mulmx; apply/matrixP=> j k; rewrite !mxE. rewrite -(inj_eq (@ord_inj _)) lift0. by rewrite (eqn_leq _ i) (leqNgt _ i) (ltn_ord i) subr0. have H2: forall i : 'I_(size p).-2.+1, (A ^+ i) *m col ord0 1%:M = col i 1%:M. case; elim=> [Hi|i IH Hi] /=. by rewrite expr0 mul1mx; congr col; apply: ord_inj. rewrite exprS -mulmxA (IH (ltnW Hi)). have Ho: (i < (size p).-2)%N by rewrite -ltnS. have ->: (Ordinal (ltnW Hi)) = (widen_ord (leqnSn (size p).-2) (Ordinal Ho)). by apply: ord_inj. by rewrite H; congr col; apply: ord_inj; rewrite lift0. case Hq: (q == 0)=> //. have Hsq: (0 < size q)%N by rewrite size_poly_gt0 Hq. rewrite /horner_mx /horner_morph horner_coef. rewrite size_map_poly_id0 ?fmorph_eq0 ?lead_coef_eq0 ?Hq // => H1 Hb. have Hw: (size q <= (size p).-2.+1)%N by rewrite -(prednK Hsq). suff : q == 0 by rewrite Hq. have: \sum_(i < size q) q`_i *: (A ^+ i *m col ord0 1%:M) = 0. rewrite (eq_bigr (fun i : 'I_(size q) => ((map_poly scalar_mx q)`_i * A ^+ i) *m col ord0 1%:M)). by rewrite -mulmx_suml ?Hb ?mul0mx //. by move=> i _; rewrite coef_map scalemxAl -mul_scalar_mx. set b := \sum_(_ < _) _. have <-: \col_(i < (size p).-2.+1) q`_i = b. apply/matrixP=> i j; rewrite mxE summxE. case: (ltnP i (size q))=> Hi. rewrite (bigD1 (Ordinal Hi)) //= H2 !mxE eqxx mulr1 big1 ?addr0 //. move=> k Hk; rewrite (H2 (widen_ord Hw k)) !mxE. move/negbTE: Hk; rewrite -!(inj_eq (@ord_inj _)) /= eq_sym=> ->. by rewrite mulr0. rewrite nth_default // big1 // => k _. rewrite (H2 (widen_ord Hw k)) !mxE -(inj_eq (@ord_inj _)) /= eqn_leq. by rewrite leqNgt (leq_trans (ltn_ord k) Hi) andFb mulr0. move/matrixP=> Hc. apply/eqP/size_poly_leq0P/leq_sizeP=> j _. case: (ltnP j (size p).-2.+1)=> Hj. by move: (Hc (Ordinal Hj) ord0); rewrite !mxE. by rewrite nth_default //; apply: leq_trans Hj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) CoqEAL(ssrcomplements mxstructure)