"Later on, one should add is_derive instances to enable automated inference." @CohenCyril @lstrsrmn (copy-pasted from a PR conversation https://github.com/math-comp/analysis/pull/1819#pullrequestreview-3869331778)
"Later on, one should add is_derive instances to enable automated inference." @CohenCyril @lstrsrmn
(copy-pasted from a PR conversation #1819 (review))