Lean EReal: get liminf = -1 from a limsup = 1 theorem via negation

Given an a.s. theorem limsup (fun n => ((S n / h n : ℝ) : EReal)) atTop = 1, the liminf = -1 companion is about 10 lines. First apply the theorem to -X; the hypotheses transfer by hind.comp (fun _ x => -x), (hid k).comp measurable_neg, integral_neg', and simpa [neg_sq]. Then prove the function equality (fun n => ((∑ (-X k) ω / h n : ℝ) : EReal)) = -(fun n => ...) by ext n; simp [Finset.sum_neg_distrib, neg_div]. Finish with rw [h, EReal.limsup_neg] at hω; rw [← neg_neg (liminf _ _), hω]. EReal.limsup_neg : limsup (-v) f = -liminf v f, so there are no boundedness side conditions.