A Missing Lemma Dual to nn_integral_FTC_atLeast

[Lawrence Paulson]

It took a little work to find the right lemmas. But it's worth having these lemmas in the long run.

> On 14 Feb 2026, at 12:12, 伊藤洋介 <glacier345 at gmail.com> wrote:
> 
> Thank you for the reply.
> I was surprised since I could not find a proof by symmetry.
> I am looking forward to seeing the proof.
> 
> 
> 2026年2月14日(土) 21:02 Lawrence Paulson <lp15 at cam.ac.uk>:
> Thanks for the suggestion. I did this and I was able to find a proof by symmetry, avoiding a near-repetition of the previous proof.
> 
> > On 11 Feb 2026, at 12:57, 伊藤洋介 <glacier345 at gmail.com> wrote:
> > 
> > Dear Isabelle developers,
> > 
> > Could you consider adding the following code to Equivalence_Lebesgue_Henstock_Integration.thy?
> > This is the counterpart of the lemma nn_integral_FTC_atLeast.
> > 
> 
> 
>