Added differentiability of the max function #5018

Job	Run time
rocq-core	48s
rocq-elpi	48s
stdlib	50s
coq	48s
coq-elpi	47s
hierarchy-builder	55s
mathcomp-bigenough	52s
mathcomp-finmap	50s
mathcomp	51s
mathcomp-analysis-single	17m 49s
mathcomp-classical	3m 4s
mathcomp-reals	2m 7s
mathcomp-reals-stdlib	1m 35s
mathcomp-analysis	15m 56s
mathcomp-experimental-reals	1m 50s
mathcomp-analysis-stdlib	1m 1s
	50m 51s

Provide feedback