Commit 2025-03-02 22:13 a3fca9d6

feat: the integral of a function bounded by a constant is less than this constant (#22467) Sometimes after a sequence of rewrites one can end up wanting to prove ∫ x, f x ∂μ ≤ c, where f is a complicated expression but which turns out to be bounded by c. To avoid stating have hf x : f x ≤ c, which can be painful because f is complicated, we introduce the lemma lintegral_le_const which directly asks to prove hf.