Small regressions with FPA

[bclement-ocp]

We are losing a few proofs on our internal dataset (less than 0.05% of the dataset) with AE 2.6.

This seems to be due to an interaction between #1041 and #1108. I don't think it is necessarily worth fixing for 2.6 (we have improvements in other areas and the loss is tiny), but I want to make sure this is not a stupid bug in the new intervals module.

(Interestingly, loading the FPA prelude twice makes the proofs pass again, which made debugging interesting due to #1235 )

[bclement-ocp]

After investigations, it does not look like it is a problem with the new intervals module, but rather a pre-existing incompleteness issue in either the arithmetic or FPA modules (in some cases using --disable-weaks makes the proof pass, in others removing unused definitions makes the proof either pass with the new intervals module or fail with the old one), we just got a bit unlucky.

Leaving this open to investigate the issue further, but I don't think it should be blocking 2.6 any longer.