refactor(Analysis): golf Mathlib/Analysis/Asymptotics/SpecificAsymptotics (leanprover-community#40068)

- rewrites `Asymptotics.isLittleO_pow_pow_cobounded_of_lt` via `mul_isLittleO` and `isLittleO_const_id_cobounded`, avoiding the explicit cobounded estimate

Extracted from leanprover-community#37968

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -44,18 +44,9 @@ open Bornology
 
 theorem Asymptotics.isLittleO_pow_pow_cobounded_of_lt (hpq : p < q) :
     (· ^ p) =o[cobounded R] (· ^ q) := by
-  nontriviality R
-  have noc : NormOneClass R := NormMulClass.toNormOneClass
-  refine IsLittleO.of_bound fun c cpos ↦ ?_
-  rw [← Nat.sub_add_cancel hpq.le]
-  simp_rw [pow_add, norm_mul, norm_pow, eventually_iff_exists_mem]
-  refine ⟨{y | c⁻¹ ≤ ‖y‖ ^ (q - p)}, ?_, fun y my ↦ ?_⟩
-  · have key : Tendsto (‖·‖ ^ (q - p)) (cobounded R) atTop :=
-      (tendsto_pow_atTop (Nat.sub_ne_zero_iff_lt.mpr hpq)).comp tendsto_norm_cobounded_atTop
-    rw [tendsto_atTop] at key
-    exact mem_map.mp (key c⁻¹)
-  · rw [← inv_mul_le_iff₀ cpos]
-    gcongr; exact my
+  rw [← Nat.add_sub_of_le hpq.le]
+  simpa [pow_add] using (isBigO_refl (· ^ p) (cobounded R)).mul_isLittleO
+    ((isLittleO_const_id_cobounded 1).pow (Nat.sub_pos_of_lt hpq))
 
 theorem Asymptotics.isBigO_pow_pow_cobounded_of_le (hpq : p ≤ q) :
     (· ^ p) =O[cobounded R] (· ^ q) := by