proposition: Lemma kermxpolyM n (g : 'M_n) (p q : {poly K}) : coprimep p q -> (kermxpoly g (p * q) :=: kermxpoly g p + kermxpoly g q)%MS.
proof: Proof. case: n => [|n] in g *; first by rewrite !thinmx0. move=> /Bezout_eq1_coprimepP [[/= u v]]; rewrite mulrC [v * _]mulrC => cpq. apply/eqmxP/andP; split; last first. apply/sub_kermxP/eqmx0P; rewrite !addsmxMr [in X in (_ + X)%MS]mulrC. by rewrite !rmorphM/= !mulmxA !mulmx_ker !mul0mx !addsmx0 submx_refl. move: cpq => /(congr1 (horner_mx g))/=; rewrite rmorph1 rmorphD/=. rewrite -[X in (X <= _)%MS]mulr1 => <-; rewrite mulrDr [p * u]mulrC addrC. rewrite addmx_sub_adds//; apply/sub_kermxP; rewrite mulmxE -mulrA -rmorphM. by rewrite mulrAC [q * p]mulrC rmorphM/= mulrA -!mulmxE mulmx_ker mul0mx. rewrite -[_ * _ * q]mulrA [u * _]mulrC. by rewrite rmorphM mulrA -!mulmxE mulmx_ker mul0mx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)