lintegral_Ioc_layervol_le

lemma lintegral_Ioc_layervol_le {a b : ℕ} : ∫⁻ t in Ioc (a : ℝ) b, layervol (X := X) k n t ≤    (b - a : ℕ) * layervol (X := X) k n (a + 1) := by  calc    _ = ∑ l ∈ Finset.Ico a b, ∫⁻ t in Ioc (l : ℝ) (l + 1), layervol (X := X) k n t := by      nth_rw 1 [← mul_one (a : ℝ), ← mul_one (b : ℝ)]      convert lintegral_Ioc_partition zero_le_one using 4; simp    _ = ∑ l ∈ Finset.Ico a b, layervol (X := X) k n (l + 1) := by      congr! 2; exact lintegral_Ioc_layervol_one    _ ≤ ∑ l ∈ Finset.Ico a b, layervol (X := X) k n (a + 1) :=      Finset.sum_le_sum fun l ml ↦ antitone_layervol (by simp_all)    _ = _ := by rw [Finset.sum_const, Nat.card_Ico, nsmul_eq_mul]