A Missing Lemma Dual to nn_integral_FTC_atLeast

[Lawrence Paulson]

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.
>