[Merged by Bors] - feat(analysis/special_functions/pow): add nnreal variant of rpow_pos

[Ruben-VandeVelde]

This matches the lemma for ennreal.

---

[Ruben-VandeVelde]

Not sure if this is worth it:

 lemma ennreal.rpow_pos {p : ℝ} {x : ℝ≥0∞} (hx_pos : 0 < x) (hx_ne_top : x ≠ ⊤) : 0 < x^p :=
 begin
-  cases lt_or_le 0 p with hp_pos hp_nonpos,
-  { exact rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos), },
-  { rw [←neg_neg p, rpow_neg, inv_pos],
-    exact rpow_ne_top_of_nonneg (by simp [hp_nonpos]) hx_ne_top, },
+  lift x to ℝ≥0 using hx_ne_top,
+  rw [ennreal.coe_pos] at hx_pos,
+  rw [ennreal.coe_rpow_of_ne_zero hx_pos.ne', ennreal.coe_pos],
+  exact nnreal.rpow_pos hx_pos,
 end

[jcommelin]

I think it doesn't matter too much.

Let's get this merged.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests