remove some edgy SMTs in Xreal and related

These might enable a version bump on some provers.

Author: fdupress

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().

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.