proposition: Lemma sizeY_mulX u : sizeY (u * 'X) = sizeY u.
proof: Proof. rewrite !sizeYE rmorphM /= swapXY_X rreg_size //. by have /monic_comreg[_ /rreg_lead] := monicX R. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype tuple finfun bigop fingroup perm div) mathcomp(ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly binomial)