Added differentiability of the max function

[lstrsrmn]

Added a lemma for showing \max is differentiable

Added two lemmas for differentiating the max function when the order is known at the point.

Motivation for this change

Differentiability of max can be useful and is general enough it should be added to the library.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Thanks for the contribution.
max_diffl should rather be called derive1_maxl by the look of existing lemmas.
I pushed force because of a rebase w.r.t. master (to get the changelog right).

[lstrsrmn]

Hello, Thank you for you help.
I am currently trying to rework the main proof into a better format

Fact der_max f g x v :
  f x <> g x -> derivable f x v -> derivable g x v ->
  (fun h => h^-1 *: (((f \max g) \o shift x) (h *: v) - (f \max g) x)) @
    0^' --> if f x < g x then 'D_v g x else 'D_v f x.

So that its more general and fits with the library more. Should I redraft this pr or make a new one with an update from this format to the newer better one?

[lstrsrmn]

Sorry I made a mistake and merged the wrong branch, should be fixed now.

A few helpful lemmas were added to classical/functions.v which are about order but rely on funext so they can't be in mathcomp order.

[lstrsrmn]

Its worth noting that the removal of the dependence on v != 0 many lemmas had in derive.v will lead to incompatibility with previous versions of Analysis

[affeldt-aist]

Before all, sincere apologies for the slow reactivity, February has been busy.
Your PR will now be treated quickly.

Sorry I made a mistake and merged the wrong branch, should be fixed now.

No harm!

Its worth noting that the removal of the dependence on v != 0 many lemmas had in derive.v will lead to incompatibility with previous versions of Analysis

Indeed, but this is a strict generalization, so dependencies that will break will be easily fixed and to the benefit of the user. The "Generalized" entry of the changelog should be appropriate to document these changes.

I have updated the changelog and also made a linting pass on the code (a bit of shortening and formatting to abide by the contributing guide https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md).

I think that we need to take another look at the naming of lemmas before merging.

[CohenCyril]

Except for the der_max thing, I think this is ready.
Later on, one should add is_derive instances to enable automated inference.

[CohenCyril]

Fact cannot yet be made private. I recommend calling it der_max_subproof to hide it.