proposition: Lemma max_size_lead_coefXY u : size (lead_coef u) <= sizeY u.
proof: Proof. by rewrite lead_coefE max_size_coefXY. 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)