ereal inverse + simplification mule and mule_def #594

Job	Run time
coq	43s
mathcomp-classical	2m 46s
mathcomp-analysis-single	13m 13s
mathcomp-reals	1m 57s
mathcomp-analysis	10m 45s
mathcomp-experimental-reals	1m 46s
mathcomp-reals-stdlib	1m 28s
ssprove	5m 6s
mathcomp-analysis-stdlib	1m 45s
	39m 29s

Provide feedback