proposition: Lemma ltr_pXz2r n (hn : 0 < n) : {in >= 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.
proof: Proof. exact: leW_mono_in (ler_pXz2r _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)