Commit 2023-08-13 11:39 14430ef6

feat: lemma limsup_const_add + 7 variants (#6455) Add 8 lemmas: limsup_const_add, ..., liminf_sub_const. The 4 lemmas about add are proven with typeclass assumptions which apply to ℝ, ℝ≥0, and ℝ≥0∞ (at least). The 4 lemmas about sub are proven with typeclass assumptions which apply to ℝ and ℝ≥0 (at least). For ℝ≥0∞, we add separate implementations of these latter 4 lemmas ENNReal.liminf_sub_const, ...