proposition: Fact ler_wpeXz2l x (x1 : 1 <= x) : {in >= 0 &, {homo exprz x : x y / x <= y}}.
proof: Proof. move=> [] m [] n; rewrite -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _. by rewrite lez_nat -?exprnP=> /ler_weXn2l; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)