proposition: Lemma ler_pXz2r n (hn : 0 < n) : {in >= 0 & , {mono ((@exprz R)^~ n) : x y / x <= y}}.
proof: Proof. apply: le_mono_in (inj_homo_lt_in _ _). by move=> x y hx hy /=; apply: pexpIrz; rewrite // gt_eqF. by apply: ler_wpXz2r; rewrite ltW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)