proposition: Lemma ieexprIz x (x0 : 0 < x) (nx1 : x != 1) : injective (exprz x).
proof: Proof. apply: wlog_lt=> // m n hmn; first by move=> hmn'; rewrite hmn. move=> /(f_equal ( *%R^~ (x ^ (- n)))). rewrite -!expfzDr ?gt_eqF // subrr expr0z=> /eqP. by rewrite pexprz_eq1 ?(ltW x0) // (negPf nx1) subr_eq0 orbF=> /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)