proposition: Lemma ler_wpiXz2l x (x0 : 0 <= x) (x1 : x <= 1) : {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_wiXn2l; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)