Merge pull request #1813 from affeldt-aist/fixes_1789 #1251

Job	Run time
rocq-core	54s
coq	55s
mathcomp-classical	57s
mathcomp-analysis-single	14m 2s
mathcomp-reals	52s
mathcomp-reals-stdlib	58s
mathcomp-experimental-reals	54s
mathcomp-analysis	51s
ssprove	5m 52s
mathcomp-analysis-stdlib	55s
	27m 10s

Provide feedback