From 7270f8c5ccfa0444c2f720bca9335733635e814a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= <fdupress@gmail.com>
Date: Tue, 27 Aug 2024 12:44:02 +0100
Subject: [PATCH] remove some edgy SMTs in Xreal and related

These might enable a version bump on some provers.
---
 examples/ehoare/adversary.ec |  2 +-
 theories/datatypes/Xreal.ec  | 12 ++++++++++--
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/examples/ehoare/adversary.ec b/examples/ehoare/adversary.ec
index f2c93e0b5d..1f22debbc2 100644
--- a/examples/ehoare/adversary.ec
+++ b/examples/ehoare/adversary.ec
@@ -91,7 +91,7 @@ proof.
   + auto => &hr /=.
     case: (O.c{hr} = Q) => [ -> /= | *].
     + rewrite Ep_mu (:(fun (a : r) => a \in O.log{hr}) = mem O.log{hr}); 1: by auto.
-      smt(mu_mem_le_mu1 size_ge0 mu_bounded dr_mu1).
+      rewrite -of_realM /=; smt(mu_mem_le_mu1 size_ge0 eps_ge0 dr_mu1).
     case: (Q < O.c{hr}); by smt().
   auto => &hr /=; apply xle_cxr => *; split; 1:smt().
   have -> /=: (Q < O.c{hr} + 1) = (Q <= O.c{hr}) by smt().
diff --git a/theories/datatypes/Xreal.ec b/theories/datatypes/Xreal.ec
index 169a09587e..e84ca54d2e 100644
--- a/theories/datatypes/Xreal.ec
+++ b/theories/datatypes/Xreal.ec
@@ -354,7 +354,11 @@ proof. by move=> /(xler_addr z) h1 /(xler_addl y); apply xle_trans. qed.
 lemma xler_pmul2l (x:realp) : 0%rp < x => 
   forall (y z : xreal),
   rp x * y <= rp x * z <=> y <= z.
-proof. move=> hx y z; case: z => // z; case: y => // y; smt(to_realP). qed.
+proof.
+rewrite (of_realK 0%r) //.
+move=> hx y z; case: z => // z; case: y => // y.
+by rewrite /= -!to_realM !to_realM ler_pmul2l.
+qed.
 
 lemma xler_wpmul2l (x : realp) (y z : xreal) :
   y <= z => x%xr * y <= x%xr * z.
@@ -363,7 +367,11 @@ proof. case: z => // z; case: y => // y; smt(to_realP). qed.
 lemma xler_pmul2r (x:realp) : 0%rp < x => 
   forall (y z : xreal),
   y * rp x <= z * rp x <=> y <= z.
-proof. move=> hx y z; case: z => // z; case: y => // y; smt(to_realP). qed.
+proof.
+rewrite (of_realK 0%r) //.
+move=> hx y z; case: z => // z; case: y => // y.
+by rewrite /= -!to_realM !to_realM ler_pmul2r.
+qed.
 
 lemma xler_wpmul2r (x : realp) (y z : xreal) :
   y <= z => y * x%xr <= z * x%xr.