proposition: Lemma sizeYE u : sizeY u = size (swapXY u).
proof: Proof. apply/eqP; rewrite eqn_leq; apply/andP; split. apply/bigmax_leqP=> /= i _; apply/leq_sizeP => j /(nth_default 0) u_j_0. by rewrite -coef_swapXY u_j_0 coef0. apply/leq_sizeP=> j le_uY_j; apply/polyP=> i; rewrite coef_swapXY coef0. by rewrite nth_default // (leq_trans _ le_uY_j) ?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)