proposition: Lemma powR_injective r : 0 < r -> {in Num.nneg &, injective (powR ^~ r)}.
proof: Proof. move=> r0 x y x0 y0; rewrite /powR; case: ifPn => [/eqP ->|xneq0]. by case: ifPn => [/eqP ->//|_ /eqP]; rewrite (gt_eqF r0) eq_sym expR_eq0. case: ifPn => [/eqP -> /eqP|yneq0]; first by rewrite (gt_eqF r0) expR_eq0. by move/expR_inj/mulfI => /(_ (negbT (gt_eqF r0))); apply: ln_inj; rewrite posrE lt_neqAle eq_sym (xneq0,yneq0). Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex