in the following PR https://github.com/math-comp/analysis/pull/1869/ by @CohenCyril https://github.com/math-comp/analysis/pull/1869#discussion_r2878372698
in the following PR #1869 by @CohenCyril
#1869 (comment)