proposition: Lemma ler_wnXz2r n (hn : n <= 0) : {in > 0 & , {homo (@exprz R)^~ n : x y /~ x <= y}}.
proof: Proof. move=> x y /= hx hy hxy; rewrite -lef_pV2 ?[_ \in _]exprz_gt0 //. by rewrite !invr_expz ler_wpXz2r ?[_ \in _]ltW // oppr_cp0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)