feat(data/real/ennreal): make of_real_sub easier to rewrite with (#16621)

A tiny edit to make this lemma more general for the purpose of rewriting - previously `q` was only for `nnreal` (even though it had the assumption of nonnegativity). 



Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>

Author: b-mehta

src/data/real/ennreal.lean

@@ -1603,7 +1603,7 @@ eq_comm.trans of_real_eq_zero
 
 alias of_real_eq_zero ↔ _ of_real_of_nonpos
 
-lemma of_real_sub (p : ℝ) (hq : 0 ≤ q) :
+lemma of_real_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) :
   ennreal.of_real (p - q) = ennreal.of_real p - ennreal.of_real q :=
 begin
   obtain h | h := le_total p q,