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.