proposition: Lemma ler_wniXz2l x (x0 : 0 <= x) (x1 : x <= 1) : {in < 0 &, {homo exprz x : x y /~ x <= y}}.
proof: Proof. move=> [] m [] n; rewrite ?NegzE -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _. rewrite lerN2 lez_nat -?invr_expz=> hmn; have := x0. rewrite le0r=> /predU1P [->|lx0]; first by rewrite !exp0rz invr0. by rewrite lef_pV2 -?topredE /= ?exprz_gt0 // ler_wiXn2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)