filter_upwards [Iic_mem_atBot 0] with y hy using
  by rw [rpow_neg (neg_nonneg.mpr hy), inv_eq_one_div, rpow_two, neg_sq]
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ (fun y => 1 / y ^ 2) =ᶠ[atBot] fun y => (-y) ^ (-2)
no goals