Added differentiability of the max function #511

Job	Run time
coq	1m 24s
mathcomp-classical	3m 9s
mathcomp	57s
mathcomp-analysis-single	16m 51s
mathcomp-reals	2m 23s
mathcomp-experimental-reals	3m 30s
mathcomp-analysis	16m 40s
mathcomp-reals-stdlib	2m 58s
mathcomp-analysis-stdlib	1m 55s
ssprove	7m 53s
	57m 40s

Provide feedback