proposition: Lemma nexpIrz n (n0 : n != 0) : {in <= 0 &, injective ((@exprz R)^~ n)}.
proof: Proof. move=> x y; rewrite ![_ \in _]le_eqVlt => /predU1P [-> _ /eqP|hx]. by rewrite exp0rz ?(negPf n0) eq_sym expfz_eq0=> /andP [_ /eqP->]. case/predU1P=> [-> /eqP|hy]. by rewrite exp0rz ?(negPf n0) expfz_eq0=> /andP [_ /eqP]. move=> /(f_equal ( *%R^~ (y ^ (- n)))) /eqP. rewrite -expfzDr ?(lt_eqF hy) // subrr expr0z -exprz_inv -expfzMl. rewrite pexprz_eq1 ?(negPf n0) /= ?mulr_le0 ?invr_le0 ?ltW //. by rewrite (can2_eq (mulrVK _) (mulrK _)) ?unitfE ?(lt_eqF hy) // mul1r=> /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)