Adapt proofs to future handling of literal constants in Coq.

This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.

1 files changed, 2 insertions, 5 deletions

diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v
index f5ccec2a..c134a3b6 100644
--- a/lib/Fappli_IEEE_extra.v
+++ b/lib/Fappli_IEEE_extra.v
@@ -746,7 +746,7 @@ Proof.
   + apply Rlt_le_trans with 0%R; auto. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply Rlt_0_1.
   + replace 1%R with (Z2R (Zfloor x) + 1)%R. apply Zfloor_ub. rewrite H. simpl. apply Rplus_0_l.
 - rewrite Ztrunc_ceil in H by (apply Rlt_le; auto). split.
-  + apply Ropp_lt_cancel. rewrite Ropp_involutive.
+  + apply (Ropp_lt_cancel (-(1))). rewrite Ropp_involutive.
     replace 1%R with (Z2R (Zfloor (-x)) + 1)%R. apply Zfloor_ub.
     unfold Zceil in H. replace (Zfloor (-x)) with 0 by omega. simpl. apply Rplus_0_l.
   + apply Rlt_le_trans with 0%R; auto. apply Rle_0_1.
@@ -1234,10 +1234,7 @@ Proof.
     { unfold eps. rewrite <- bpow_plus. replace (emin - 1 + -emin) with (-1) by omega. auto. }
     rewrite P. unfold Znearest.
     assert (F: Zfloor (/ 2)%R = 0).
-    { apply Zfloor_imp.
-      split. apply Rlt_le. apply Rinv_0_lt_compat. apply (Z2R_lt 0 2). omega.
-      change (Z2R (0 + 1)) with 1%R. rewrite <- Rinv_1 at 3. apply Rinv_1_lt_contravar. apply Rle_refl. apply (Z2R_lt 1 2). omega.
-    }
+    { apply Zfloor_imp. simpl. lra. }
     rewrite F. change (Z2R 0) with 0%R. rewrite Rminus_0_r. rewrite Rcompare_Eq by auto.
     simpl. unfold F2R; simpl. apply Rmult_0_l.
   }