From 03aa4ed741aaff5d6af9634c5eb26cfd3b0bdf8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= <fdupress@gmail.com>
Date: Fri, 21 Feb 2025 18:00:44 +0000
Subject: [PATCH] start removing our blessing from alt-ergo

---
 easycrypt.project                        |  1 -
 examples/MEE-CBC/RCPA_CMA.ec             |  2 +-
 examples/PIR.ec                          | 10 ++-
 examples/ehoare/qselect/partition.eca    |  4 +-
 examples/hashed_elgamal_std.ec           |  2 +-
 theories/algebra/DynMatrix.eca           | 26 +++++---
 theories/analysis/RealFLub.ec            | 16 +++--
 theories/analysis/RealFun.ec             |  2 +-
 theories/analysis/RealLub.ec             | 14 ++--
 theories/analysis/RealSeries.ec          |  3 +-
 theories/crypto/PROM.ec                  | 20 ++++--
 theories/crypto/PRP.eca                  | 32 ++++++---
 theories/crypto/SplitRO.ec               |  7 +-
 theories/crypto/assumptions/DHIES.ec     | 70 ++++++++++++--------
 theories/crypto/assumptions/PKSMK.ec     |  8 +--
 theories/crypto/prp_prf/Strong_RP_RF.eca |  8 ++-
 theories/datatypes/List.ec               | 37 +++++++++--
 theories/datatypes/MSet.ec               |  8 ++-
 theories/datatypes/Word.eca              |  7 +-
 theories/datatypes/Xreal.ec              | 83 ++++++++++++++++++++++--
 theories/distributions/DInterval.ec      |  2 +-
 theories/distributions/DList.ec          |  9 ++-
 theories/distributions/Distr.ec          | 21 +++---
 theories/distributions/Mu_mem.ec         |  9 ++-
 theories/distributions/SDist.ec          | 13 ++--
 theories/encryption/Hybrid.ec            |  3 +-
 26 files changed, 308 insertions(+), 109 deletions(-)

diff --git a/easycrypt.project b/easycrypt.project
index f592382998..727e5f7819 100644
--- a/easycrypt.project
+++ b/easycrypt.project
@@ -1,4 +1,3 @@
 [general]
-provers = Alt-Ergo@2.4
 provers = CVC5@1.0
 provers = Z3@4.12
diff --git a/examples/MEE-CBC/RCPA_CMA.ec b/examples/MEE-CBC/RCPA_CMA.ec
index 1660746704..574dcbe099 100644
--- a/examples/MEE-CBC/RCPA_CMA.ec
+++ b/examples/MEE-CBC/RCPA_CMA.ec
@@ -336,7 +336,7 @@ theory EtM.
     type leaks           <- leaks,
     op   leak            <- leak,
     op   dC    (l:leaks) <- (dC l) `*` (MUnit.dunit witness<:tag>)
-  proof * by smt.
+  proof * by smt(dprod_ll dC_ll dunit_ll).
 
   (** The black-box construction is as follows **)
   module EtM(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = {
diff --git a/examples/PIR.ec b/examples/PIR.ec
index 01dc3932f7..41317f0e71 100644
--- a/examples/PIR.ec
+++ b/examples/PIR.ec
@@ -22,7 +22,13 @@ proof. by exists [] s. qed.
 
 lemma sxor2_cons (s s':int list) (i j:int):
   sxor2 s s' i => sxor2 (j::s) (j::s') i.
-proof. smt (). qed.
+proof.
+move=> [].
+  move=> [] s1 s2 [] -> ->.
+  by left; exists (j :: s1) s2.
++ move=> [] s1 s2 [] -> ->.
+  by right; exists (j :: s1) s2.
+qed.
 
 (* The database *)
 op a : int -> word.
@@ -72,7 +78,7 @@ proof.
     while (j <= N /\ if j <= i then PIR.s = PIR.s' else sxor2 PIR.s PIR.s' i).
     + wp;rnd;skip => /= &m [[_]] + HjN.
       have -> /= : j{m} + 1 <= N by smt ().
-      case: (j{m} <= i{m}) => Hji;2: by smt ().
+      case: (j{m} <= i{m})=> Hji; 2:smt(sxor2_cons).
       move=> -> b _;case: (j{m} = i{m}) => [->> | /#].
       by rewrite (_ : !(i{m}+1 <= i{m})) 1:/# /=; smt (sxor_cons).
     by auto => /#.
diff --git a/examples/ehoare/qselect/partition.eca b/examples/ehoare/qselect/partition.eca
index b0148dbddb..edba6f6420 100644
--- a/examples/ehoare/qselect/partition.eca
+++ b/examples/ehoare/qselect/partition.eca
@@ -100,7 +100,9 @@ lemma index_count x l: sorted (<=) l => uniq l => x \in l => index x l = count (
 proof.
   elim: l => // y l hrec /> hp hnin hu.
   case: (x = y) => [<<- _ | hne /= hin] /=.
-  + by rewrite index_cons /= count_pred0_eq_in //=; smt (order_path_min allP le_trans lt_nle).
+  + rewrite index_cons /= count_pred0_eq_in //=; 2:smt(lt_nle).
+    move=> x0 x0_in_l; move: (order_path_min (<=) le_trans x l hp).
+    by rewrite allP=> /(_ _ x0_in_l); rewrite lt_nle.
   rewrite index_cons hne /= hrec //; 1: by apply: path_sorted hp.
   smt (order_path_min allP le_trans).
 qed.
diff --git a/examples/hashed_elgamal_std.ec b/examples/hashed_elgamal_std.ec
index 9792376147..03bfa02a86 100644
--- a/examples/hashed_elgamal_std.ec
+++ b/examples/hashed_elgamal_std.ec
@@ -192,7 +192,7 @@ section Security.
             - Pr[ES1(ESAdv(A)).main() @ &m : res]|.
   proof.
   rewrite (cpa_ddh0 &m) (ddh1_es1 &m) (es0_Gb &m) (Gb_half &m).
-  smt(@Real).
+  smt(StdOrder.RealOrder.ler_dist_add).
   qed.
 end section Security.
 
diff --git a/theories/algebra/DynMatrix.eca b/theories/algebra/DynMatrix.eca
index a3ce6bacbf..8338e31700 100644
--- a/theories/algebra/DynMatrix.eca
+++ b/theories/algebra/DynMatrix.eca
@@ -73,7 +73,8 @@ lemma offunvK pv: tofunv (offunv pv) = vclamp pv.
 proof. by rewrite /tofunv /offunv eqv_repr vclamp_idemp. qed.
 
 lemma vectorW (P : vector -> bool): 
-  (forall pv, P (offunv pv)) => forall v, P v by smt(tofunvK).
+  (forall pv, P (offunv pv)) => forall v, P v.
+proof. by move=> P_pv v; rewrite -tofunvK; apply: P_pv. qed.
 
 (* Dimension of the vector *)
 op size v = (tofunv v).`2.
@@ -593,8 +594,10 @@ qed.
 lemma dvector1E (d : R distr) (v : vector) : mu1 (dvector d (size v)) v =
   BRM.bigi predT (fun i => mu1 d v.[i]) 0 (size v).
 proof.
-rewrite -{2}[v]tolistK dmapE /(\o) /pred1. 
-rewrite (@mu_eq _ _ (pred1 (tolist v))); 1: smt(oflist_inj).
+rewrite -{2}[v]tolistK dmapE /(\o) /pred1.
+rewrite (@mu_eq _ _ (pred1 (tolist v))).
++ move=> x; rewrite eq_iff /pred1 /=; split=> />.
+  exact: oflist_inj.
 rewrite dlist1E 1:/# size_tolist max0size /=.
 by rewrite BRM.big_mapT /(\o) &BRM.eq_big.
 qed.
@@ -694,7 +697,8 @@ proof. by rewrite /tofunm /offunm eqv_repr. qed.
 hint simplify offunmK.
 
 lemma matrixW (P : matrix -> bool) : (forall pm, P (offunm pm)) =>
-  forall m, P m by smt(tofunmK).
+  forall m, P m.
+proof. by move=> P_pm m; rewrite -tofunmK; exact: P_pm. qed.
 
 (* Number of rows and columns of matrices *)
 op rows m = (tofunm m).`2.
@@ -1451,16 +1455,17 @@ qed.
 lemma catmrA (m1 m2 m3: matrix): ((m1 || m2) || m3) = (m1 || (m2 || m3)).
 proof. 
 rewrite eq_matrixP. 
-split => [| i j bound]; 1: smt(size_catmr).
+split => [| i j bound]; 1:smt(size_catmr rows_catmr cols_catmr).
 rewrite 4!get_catmr cols_catmr // addrA. 
-algebra.
+by algebra.
 qed.
 
 lemma catmrDr (m1 m2 m3: matrix): m1 * (m2 || m3) = ((m1 * m2) || (m1 * m3)).
 proof.
 rewrite eq_matrixP.
 rewrite rows_mulmx cols_mulmx cols_catmr.
-split => [| i j bound]; 1: smt(size_mulmx size_catmr).
+split => [| i j bound].
++ by rewrite !size_catmr !rows_mulmx !cols_mulmx /#.
 rewrite get_catmr 3!get_mulmx. 
 case (j < cols m2) => bound2.
 - rewrite [col m3 _]col0E 1:/# dotpv0 addr0 !dotpE 2!size_col rows_catmr.
@@ -1667,7 +1672,9 @@ case (j < n) => j_bound.
   + smt(size_catmr size_subm).
   by rewrite addr0.
 - rewrite getm0E; 1: smt(size_catmr size_subm).
-  rewrite add0r get_subm; smt(size_catmr size_subm).
+  rewrite add0r get_subm; [3:smt()].
+  + smt(rows_catmr rows_subm).
+  + smt(cols_catmr cols_subm).
 qed.
 
 lemma subm_colmx (m: matrix) l : 
@@ -1908,7 +1915,8 @@ move => r_ge0 c_ge0; split => [m_supp|]; last first.
 - case => -[r_m c_m] m_d; rewrite /support -r_m -c_m dmatrix1E.
   apply prodr_gt0_seq => i i_row _ /=.
   by apply prodr_gt0_seq => j j_col _ /=; apply m_d; smt(mem_iota).
-have [r_m c_m] : size m = (r,c) by smt(size_dmatrix). 
+have [r_m c_m] : size m = (r,c).
++ exact: (size_dmatrix d).
 split => [//|i j range_ij]; move: m_supp. 
 rewrite -r_m -c_m /support dmatrix1E => gt0_big.
 pose G i0 := (fun (j0 : int) => mu1 d m.[i0, j0]).
diff --git a/theories/analysis/RealFLub.ec b/theories/analysis/RealFLub.ec
index 2f5e81ef0e..7294720da8 100644
--- a/theories/analysis/RealFLub.ec
+++ b/theories/analysis/RealFLub.ec
@@ -25,8 +25,10 @@ by smt().
 lemma flub_upper_bound (F : 'a -> real) x : 
     has_fub F => F x <= flub F.
 proof.
-move => H. apply lub_upper_bound; 2: by exists x.
-by split; [ by exists (F x) x | smt() ].
+move => H; apply lub_upper_bound; 2: by exists x.
+split.
++ by exists (F x) x.
+by case: H=> r is_fub_F_r; exists r=> /#.
 qed.
 
 lemma flub_le_ub (F : 'a -> real) r :
@@ -53,7 +55,10 @@ lemma flubZ (f: 'a -> real) c : has_fub f =>
   c >= 0%r => flub (fun x => c * f x) = c * flub f.
 proof.
 move => fub_f c_ge0 @/flub; pose E := fun r => exists a, f a = r.
-have -> : (fun r => exists a, c * f a = r) = scale_rset E c by smt().
+have -> : (fun r => exists a, c * f a = r) = scale_rset E c.
++ apply: fun_ext=> x; rewrite eq_iff; split.
+  + by move=> [] a xP; exists (f a); rewrite xP=> //=; exists a.
+  + by move=> /> a; exists a.
 by rewrite lub_scale //; apply has_fub_lub.
 qed.
 
@@ -61,9 +66,10 @@ lemma flub_const c :
   flub (fun _ : 'a => c) = c.
 proof.
 apply eqr_le; split; first apply flub_le_ub => /#.
-move => _; apply (@flub_upper_bound (fun _ => c) witness) => /#.
+move=> _; apply (@flub_upper_bound (fun _=> c) witness).
+by exists c=> /#.
 qed.
 
 lemma has_fubZ (f: 'a -> real) c: has_fub f =>
   c >= 0%r => has_fub (fun x => c * f x).
-proof. move => [ym ub_ym] ge0_c; exists (c * ym) => /#. qed.
+proof. by move => [ym ub_ym] ge0_c; exists (c * ym) => /#. qed.
diff --git a/theories/analysis/RealFun.ec b/theories/analysis/RealFun.ec
index 7ee825bef7..c98c0f534c 100644
--- a/theories/analysis/RealFun.ec
+++ b/theories/analysis/RealFun.ec
@@ -35,7 +35,7 @@ proof. smt (). qed.
 
 lemma convexD f1 f2 a b:
   convex f1 a b => convex f2 a b => convex (fun x => f1 x + f2 x) a b.
-proof. smt (). qed.
+proof. by move=> + + x x_in01; smt(). qed.
 
 lemma convexZ c f a b: 0%r <= c =>
   convex f a b => convex (fun x => c * f x) a b.
diff --git a/theories/analysis/RealLub.ec b/theories/analysis/RealLub.ec
index caba98790a..e2d3a73fac 100644
--- a/theories/analysis/RealLub.ec
+++ b/theories/analysis/RealLub.ec
@@ -81,8 +81,11 @@ qed.
 (* -------------------------------------------------------------------- *)
 lemma lub1 x : lub (pred1 x) = x.
 proof.
-apply eqr_le; split; [apply lub_le_ub => /#|move => _].
-apply lub_upper_bound; smt().
+have haslub_1x: (has_lub (pred1 x)).
++ by rewrite /has_lub; split; exists x=> /#.
+apply: eqr_le; split.
++ by apply: lub_le_ub=> //#.
+by move=> _; apply: lub_upper_bound.
 qed.
 
 (* -------------------------------------------------------------------- *)
@@ -102,7 +105,8 @@ qed.
 lemma has_lub_scale E c : 0%r <= c =>
   has_lub E => has_lub (scale_rset E c).
 proof.
-move => c_ge0 [[x Ex] ?]; split; 1: smt().
+move=> c_ge0 [[x Ex] ?]; split.
++ by exists (c * x) x.
 exists (c * lub E) => cx; smt(lub_upper_bound).
 qed.
 
@@ -115,7 +119,9 @@ apply eqr_le; split => [|_].
 - apply lub_le_ub; first by apply has_lub_scale.
   smt(lub_upper_bound).
 rewrite -ler_pdivl_mull //; apply lub_le_ub => // x Ex.
-by rewrite ler_pdivl_mull //; smt(lub_upper_bound has_lub_scale). 
+rewrite ler_pdivl_mull //; apply: lub_upper_bound.
++ exact: has_lub_scale.
+by exists x.
 qed.
 
 (* -------------------------------------------------------------------- *)
diff --git a/theories/analysis/RealSeries.ec b/theories/analysis/RealSeries.ec
index 07497637c3..ac61c29b7d 100644
--- a/theories/analysis/RealSeries.ec
+++ b/theories/analysis/RealSeries.ec
@@ -965,7 +965,8 @@ lemma summable_inj (h : 'a -> 'b) (s : 'b -> real) :
   injective h => summable s => summable (s \o h).
 proof.
 move => inj_h [M] sum_s; exists M => J uniq_J. 
-have R := sum_s (map h J) _; 1: rewrite map_inj_in_uniq /#.
+have R := sum_s (map h J) _.
++ by rewrite map_inj_in_uniq=> // x y _ _ /inj_h.
 apply (ler_trans _ _ R) => {R}; rewrite big_map /(\o)/= big_mkcond.
 exact Bigreal.ler_sum.
 qed.
diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec
index c2d76c7bd8..c672898f6a 100644
--- a/theories/crypto/PROM.ec
+++ b/theories/crypto/PROM.ec
@@ -287,12 +287,22 @@ fel 1 (fsize RO.m) (fun x => x%r * Pc) q (fcoll f RO.m)
 - inline*; auto; smt(fsize_empty mem_empty).
 - proc; inline*; (rcondt 2; first by auto); wp.
   rnd (fun r => exists u, u \in RO.m /\ f (oget RO.m.[u]) = f r).
-  skip => &hr; rewrite andaE => /> 3? I ?; split; 2: smt(get_setE).
-  apply mu_mem_le_fsize => u /I /(dmap_supp _ f) /fcollP /= /(_ x{hr}).
-  rewrite dmap1E. apply: StdOrder.RealOrder.ler_trans.
-  by apply mu_sub => /#.
+  auto=> /> &0 ge0_size_m ltq_size_m nocoll I x_notin_m; split=> [|_].
+  + apply mu_mem_le_fsize => u /I /(dmap_supp _ f) /fcollP /= /(_ x{0}).
+    rewrite dmap1E; apply: StdOrder.RealOrder.ler_trans.
+    by apply: mu_sub=> @/pred1 @/(\o) /> x ->.
+  move=> v _ i j; rewrite !mem_set.
+  move=> i_in_mVx j_in_mVx i_neq_j; rewrite !get_setE.
+  case: (i = x{0}); case: (j = x{0})=> />.
+  + by move=> _ coll_v; exists j=> /#.
+  + by move=> _ coll_v; exists i=> /#.
+  move=> j_neq_x i_neq_x eq_f.
+  move: nocoll=> /negb_exists /= /(_ i) /negb_exists /= /(_ j).
+  rewrite i_neq_j eq_f.
+  move: i_in_mVx; rewrite i_neq_x=> /= -> /=.
+  by move: j_in_mVx; rewrite j_neq_x=> /= -> /=.
 - move => c; proc; auto => />; smt(get_setE fsize_set).
-- move => b c. proc. by auto.
+- move => b c; proc; by auto.
 qed.
 
 end section Collision.
diff --git a/theories/crypto/PRP.eca b/theories/crypto/PRP.eca
index c92923525d..e2dc9d289f 100644
--- a/theories/crypto/PRP.eca
+++ b/theories/crypto/PRP.eca
@@ -279,15 +279,15 @@ lemma collision_add (m:(D,D) fmap) x y:
   collision m.[x <- y] <=> collision m \/ rng m y.
 proof.
 move=> x_notin_m; split=> [[z z' [z'_neq_z]]|].
-+ rewrite mem_set=> -[z_in_m] [z'_in_m] mz_eq_mz'.
++ rewrite !mem_set !get_setE=> -[z_in_m] [z'_in_m] mz_eq_mz'.
   case (rng m y)=> //= y_notin_rngm.
-  by exists z z'; smt(@SmtMap).
+  by exists z z'; smt().
 move=> [[z z' [z'_neq_z] [z_in_m] [z'_in_m] mz_eq_mz']|].
 + exists z z'; rewrite z'_neq_z !mem_set !get_setE mz_eq_mz' z_in_m z'_in_m /=.
   move/contra: (congr1 (dom m) z x); rewrite x_notin_m z_in_m=> -> //=.
   by move/contra: (congr1 (dom m) z' x); rewrite x_notin_m z'_in_m=> -> //=.
 rewrite rngE=> - /= [x'] mx'_y.
-by exists x x'; smt(@SmtMap).
+by exists x x'; rewrite !get_setE !mem_set /#.
 qed.
 
 lemma collision_stable (m:(D,D) fmap) y y':
@@ -459,7 +459,8 @@ section Upto.
                 PRFi.m{2} = RP.m.[x <- r0]{1} /\
                 ((PRP_indirect_bad.bad \/ rng RP.m r0){1} <=> collision PRFi.m{2})).
     + auto => /> &1 &2 coll _ x_notin_m r _; split=> [|x0 x'].
-      + rewrite rngE /= /collision=> - [x'] mx'; exists x{2} x'; smt(domE get_setE).
+      + rewrite rngE /= /collision=> - [x'] mx'.
+        by exists x{2} x'; rewrite !mem_set !get_setE /#.
       smt (rngE get_setE).
     sp; if{1}.
     + conseq (_: _ ==> collision PRFi.m{2} /\ PRP_indirect_bad.bad{1})=> //.
@@ -472,7 +473,9 @@ section Upto.
          [auto|if=> //=; auto|hoare; auto]=> />;rewrite ?dD_ll //.
     by move=> &hr x_notin_m r_in_rng_m; apply excepted_lossless; exists x{hr}.
     move=> &1; conseq (_: collision PRFi.m ==> collision PRFi.m: =1%r)=> //=.
-    by proc; if; auto=> />; rewrite dD_ll //=; smt(domE get_setE).
+    proc; if; auto=> />; rewrite dD_ll //=.
+    move=> &0 x x' x'_neq_x x_in_m x'_in_m x_coll_x' x0_notin_m v _ _.
+    by exists x x'=> />; rewrite !mem_set x_in_m x'_in_m /= !get_set_neqE 1,2:/#.
   inline *; auto=> />; split=> [|_].
   + by rewrite no_collision=> x x'; rewrite mem_empty.
   move=> /> rL rR DL b mL DR mR [-> //| /#].
@@ -583,15 +586,24 @@ section CollisionProbability.
   proc; inline*; wp.
   call (_: ={PRFi.m} /\
            size Sample.l{1} = card (fdom PRFi.m){2} /\
-           (forall x, mem (frng PRFi.m) x <=> mem Sample.l x){1} /\
+           (forall x, rng PRFi.m x <=> mem Sample.l x){1} /\
            (collision PRFi.m{2} <=> !uniq Sample.l{1})).
   + proc; inline*.
     if => //=.
     auto => /> &1 &2 h1 h2 h3 h4 r _.
-    rewrite fdom_set fcardUI_indep 2:fcard1; 1: by rewrite fsetI1 mem_fdom h4.
-    split; 1:smt(). 
-    split; smt(get_setE mem_frng rngE collision_add).    
-  auto; smt (size_eq0 fdom0 fcards0 frng0 in_fset0 mem_empty).
+    rewrite fdom_set fcardUI_indep 2:fcard1; 1:by rewrite fsetI1 mem_fdom h4.
+    split; 1:smt().
+    split.
+    + move=> v; rewrite -h2 !rngE /=; split.
+      + move=> [] x0; rewrite get_setE; case: (x0 = x{2})=> /> _ m_x0.
+        by right; exists x0.
+      + case=> />.
+        + by exists x{2}; rewrite get_set_sameE.
+        + move=> x0 m_x0; exists x0; rewrite get_set_neqE //.
+          rewrite domE in h4; rewrite -negP=> <<-.
+          by move: h4; rewrite m_x0.
+    + smt(collision_add).
+  by auto; smt (size_eq0 fdom0 fcards0 frng0 in_fset0 mem_empty).
   qed.
 
   local hoare IND_bounded : IND(PRFi,D).main : true ==> card (fdom PRFi.m) <= q.
diff --git a/theories/crypto/SplitRO.ec b/theories/crypto/SplitRO.ec
index bbf6642536..75ecb2237f 100644
--- a/theories/crypto/SplitRO.ec
+++ b/theories/crypto/SplitRO.ec
@@ -162,7 +162,12 @@ section PROOFS.
         by rewrite /pred1 /(\o) (can_eq _ _ ofpairK).
       move=> _ t; rewrite sample_spec supp_dmap => -[[t1 t2] []] + ->>.
       by rewrite topairK ofpairK => ->.
-    by auto => />; smt (get_setE map_set set_pair_map mem_map mem_pair_map mem_set mapE mergeE).
+    auto=> /> &2 eq_dom; move: (eq_dom x{2}); rewrite !eq_iff.
+    rewrite !mem_map !mem_pair_map !mapE !mergeE 1:/o_pair //.
+    case _: (x{2} \in I1.RO.m{2})=> />.
+    + by rewrite !domE; case: (I1.RO.m.[x]{2})=> />; case: (I2.RO.m.[x]{2}).
+    rewrite !get_set_sameE /= -(map_set (fun _=> ofpair)) set_pair_map /=.
+    by move=> + + x0; rewrite mem_map mem_pair_map !mem_set /#.
   qed.
 
   equiv RO_split: 
diff --git a/theories/crypto/assumptions/DHIES.ec b/theories/crypto/assumptions/DHIES.ec
index 183287d30e..66437a0eb6 100644
--- a/theories/crypto/assumptions/DHIES.ec
+++ b/theories/crypto/assumptions/DHIES.ec
@@ -211,8 +211,10 @@ theory DHIES.
     rewrite equiv[{1} 1 EncDHIES_map.sample].
     inline*; auto=> /> &m i_le_kks i_ge_0.
     rewrite (nth_map witness witness (snd \o snd)); 1: smt().
-    rewrite (drop_nth witness i{m}) /#.
-  by auto=> />; smt(drop_le0 size_map).
+    by rewrite (drop_nth witness i{m}) /#.
+  auto=> /> &2; rewrite !size_map drop_size //=.
+  split=> [/#|i l _ /ltzNge i_lt0 _].
+  by rewrite drop_le0 1:/#.
   qed.
 
   clone import DProd.DLetSampling as MRnd_let
@@ -424,8 +426,8 @@ lemma mem_mencDHIES cphs tag ptxt kk:
 proof.
 rewrite supp_djoinmap; move=> [Hsz /allP H].
 rewrite -(map_snd_zip _ kk) // -(map_fst_zip _ kk cphs) //.
-apply eq_in_map; rewrite /(\o) /= => *.
-by move: (H _ H0) => /=; rewrite supp_dmap; move=> [y [Hy1 /= ->]].
+apply eq_in_map; rewrite /(\o)=> /= x x_in_zip.
+by move: (H _ x_in_zip)=> /=; rewrite supp_dmap=> - [y [Hy1 /= ->]].
 qed.
 
 lemma ephmem_foldenc pk t c pks tag ptxt mctxt kk:
@@ -434,7 +436,7 @@ lemma ephmem_foldenc pk t c pks tag ptxt mctxt kk:
  (pk,t,c) \in fold_encs pks tag (FMap.ofassoc mctxt) =>
  c.`1 = fst (oget (assoc kk pk)).
 proof.
-move=> Hin2 /mem_mencDHIES Hmap ? .
+move=> Hin2 /mem_mencDHIES Hmap H.
 move: (Hin2); move: (eq_keys_amap _ _ _ _ Hmap) => <- Hin1.
 rewrite -(Core.oget_omap_some fst (assoc kk pk)).
 by apply/assocTP.
@@ -503,15 +505,17 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
       move=> /= ? ?.
       rewrite joinE; pose E := (_ \in _)%FMap; case: E; rewrite /E; clear E; last smt().
       rewrite -map_comp /(\o) /= ofassoc_get mem_ofassoc -map_comp /(\o) /=.
-      move=> /mapP [pk' [Hpk' /= [-> ->]]] _; smt (mem_fdom memE).
+      move=> /mapP [pk' [Hpl' /= [-> ->]]] ?.
+      move: (H8 pk'); rewrite -H0 mem_fdom; apply.
+      by move: Hpl'; rewrite memE; exact.
     + move: H16 H17 H18; rewrite !H /=.
       rewrite (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
        by apply/(supp_dlist_size _ _ _ _ H12)/size_ge0.
       move=> /= ? ?.
       rewrite joinE; pose E := (_ \in _)%FMap; case: E; rewrite /E; clear E; last smt().
       rewrite -map_comp /(\o) /= ofassoc_get.
-      move => ? ?; exists ephL.
-      move: (assoc_some _ _ _ H20) => /mapP [v [? /= [[? ?] ?]]]; smt().
+      move => ? H20; exists ephL.
+      by move: (assoc_some _ _ _ H20) => /mapP [v [? /= [[? ?] ?]]]; smt().
     + move: H16 H17; rewrite !H /=.
       rewrite (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
        by apply/(supp_dlist_size _ _ _ _ H12)/size_ge0.
@@ -520,7 +524,7 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
     + move: H16 H17; rewrite !H /=.
       rewrite (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
        by apply/(supp_dlist_size _ _ _ _ H12)/size_ge0.
-      move=> /= ? ?; move: H18; rewrite mem_cat mem_join; move=> [?|?]; first left; smt().
+      move=> /= ? H17; move: H18; rewrite mem_cat mem_join; move=> [?|H18]; first left; smt().
       right; rewrite mem_ofassoc -!map_comp /(\o) /=; apply/mapP; exists pk; split.
       + move: H18; rewrite /fold_encs; elim: (elems pks{2})=> // pk0 pks ih.
         by case: (pk = pk0)=> />.
@@ -530,15 +534,16 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
         by case: (pk = pk0)=> />.
       rewrite (ephmem_foldenc _ _ _ _ _ _ _ _ T H17 H18) /=.
       have ? : 0 <= index pk (elems pks{2}) < size (elems pks{2}).
-      + smt(index_ge0 index_mem map_comp mapP).
+      + rewrite index_ge0 index_mem /=; move: T.
+        by rewrite -map_comp mapP /(\o)=> />.
       rewrite /assoc onth_nth_map -!map_comp /(\o) /= map_id
               (nth_map witness) //=.
     + move: H16 H17 H19; rewrite !H /= (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
        by apply/(supp_dlist_size _ _ _ _ H12)/size_ge0.
       move=> /= ? ?.
       rewrite joinE; pose E := (_ \in _)%FMap; case: E; rewrite /E; clear E; last smt().
-      rewrite -map_comp /(\o) /= ofassoc_get => ? ?.
-      move: (assoc_some _ _ _ H20) => /mapP [v [? /= [[? ?] ?]]].
+      rewrite -map_comp /(\o) /= ofassoc_get => ? H20.
+      move: (assoc_some _ _ _ H20) => /mapP [v [? /= [[H22 H23] H24]]].
       rewrite H24 H23 -H22.
       move: (H4 _ _ H18) => ->; congr.
       by rewrite -!GP.expM ZPF.mulrC.
@@ -548,11 +553,11 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
    if;first by move=> /> ??? ->.
     case (((pk,ctxt.`1) \in Adv1_Procs.skeys){2}).
      rcondf {2} 1; first by auto => />.
-     wp; skip; rewrite /inv /=; clear inv => /> *.
+     wp; skip; rewrite /inv /=; clear inv => /> &1 &2 *.
      rewrite /decrypt; congr.
-     move: (eq_refl (MRPKE_lor.pklist{1}.[pk{2}])); case: {2}(MRPKE_lor.pklist{1}.[pk{2}]).
-      by smt(mem_fdom).
-     move=> sk Hpk; rewrite Hpk /=; smt (mem_fdom).
+     case _: (MRPKE_lor.pklist{1}.[pk{2}]).
+     + smt(mem_fdom).
+     by case _: (Adv1_Procs.skeys.[pk, ctxt.`1]{2})=> /#.
     rcondt {2} 1; first by auto => />.
     rcondt {2} 4.
      move => *;wp;skip; rewrite /inv /=; smt (mem_fdom).
@@ -865,14 +870,16 @@ last by wp; skip; rewrite /inv /= => />; smt (fdom0 emptyE).
      - by move: H12; rewrite zip_mapr -map_comp /(\o)/= unzip2_zip /#.
      - rewrite !zip_mapr !(map_zip_nth witness witness) /= 1,3:/#.
           rewrite size_map size_iota H10.
-           move : H12; rewrite /menc. smt(size_ge0 supp_djoinmap).
+           move : H12; rewrite /menc /= supp_djoinmap size_map size_zip size_map H10.
+           smt(size_ge0).
           rewrite H10.
-           move : H12; rewrite /menc. smt(size_ge0 supp_djoinmap).
+           move : H12; rewrite /menc /= supp_djoinmap size_map size_zip size_map H10.
+           smt(size_ge0).
        rewrite size_map /range /= size_iota ler_maxr 1:size_ge0.
        apply eq_in_map => y /mem_iota /= [? ?] /=.
        by rewrite (nth_map witness) /= 1:#smt:(size_iota) nth_iota.
      - rewrite H10.
-           move : H12; rewrite /menc. smt(size_ge0 supp_djoinmap).
+           move : H12; rewrite /menc supp_djoinmap size_map size_zip size_map H10. smt(size_ge0).
   wp; skip; rewrite /inv /=; clear inv; progress.
   + rewrite /=; congr; congr.
     have ->: (fun (cph : int * Cph) => (g ^ x{2}, cph.`2))
@@ -918,7 +925,9 @@ last by wp; skip; rewrite /inv /= => />; smt (fdom0 emptyE).
     right.
     move: H14; rewrite ofassoc_get unzip1_zip; 1: smt (size_iota size_ge0).
     move/assoc_some_onth_mem => [idx] /onth_zip_some [] /onth_map_some [pk']; progress.
-    have Hidx: (index pk' (elems pks{2})) = idx by smt (onth_some index_uniq uniq_elems).
+    have Hidx: (index pk' (elems pks{2})) = idx.
+    move: (onth_some _ _ _ H14)=> [] idx_bounded <-.
+    by rewrite index_uniq // uniq_elems.
     move:H15=> /onth_iota_some; progress.
     move: H13; rewrite mem_cat; move=> [? /#|].
     move=> /mapP [[i' c'] /=] [] /onth_mem [idx'] /onth_zip_some /= [] /onth_iota_some; progress.
@@ -950,25 +959,32 @@ last by wp; skip; rewrite /inv /= => />; smt (fdom0 emptyE).
     move: H15 => /onth_map_some [[i' c']]; progress.
     move: H15 => /onth_zip_some [] /onth_iota_some; progress.
     rewrite assoc_zip 1:#smt:(size_map) (onth_nth witness).
-    + smt (index_map onth_some index_uniq uniq_elems).
+    + rewrite (index_map (fun pk=> (pk, g^x{2}))) //.
+      move: (onth_some _ _ _ H13)=> [] idx_bounded <-.
+      by rewrite index_uniq // 1:uniq_elems /#.
     congr.
     rewrite nth_cat.
     have -> /=: !(size AEADmul_Oracles.keys{2} + idx < size AEADmul_Oracles.keys{2}) by smt().
     congr.
-    rewrite (index_map (fun (pk : Pk) => (pk, g ^ x{2}))) 1:/#.
-    smt (index_map onth_some index_uniq uniq_elems).
+    rewrite (index_map (fun (pk : Pk) => (pk, g ^ x{2}))) //.
+    move: (onth_some _ _ _ H13)=> [] idx_bounded <-.
+    by rewrite index_uniq // 1:uniq_elems /#.
 + proc.
   seq 1 1 : (#pre /\ r{1} = msg{2}); first by auto => />.
   if=> //; first by rewrite /inv.
   if=> //; first by rewrite /inv.
-   if=> //; 1: by rewrite /inv /= => /> *; smt (mem_fdom).
+  + if=> //.
+    + by rewrite /inv=> /> &1 &2; smt(mem_fdom).
     inline *.
     rcondt {2} 6.
      move=> *; wp; skip; rewrite /inv => /> *.
-     (have: exists i, Adv2_Procs.kindex{hr}.[(pk{m0}, ctxt{m0}.`1)] = Some i by smt (mem_fdom));
+     case _: (Adv2_Procs.kindex{hr}.[(pk, ctxt.`1)]{m0}).
+     + by move: H10; rewrite -mem_fdom H -H2 mem_fdom domE.
      smt ().
-    wp; skip; rewrite /inv /=; clear inv; progress;
-    (have: exists i, Adv2_Procs.kindex{2}.[(pk{2}, ctxt{2}.`1)] = Some i by smt (mem_fdom)); smt ().
+    wp; skip; rewrite /inv /=; clear inv=> /> *.
+    case _: (Adv2_Procs.kindex.[(pk, ctxt.`1)]{2}).
+    + by move: H10; rewrite -mem_fdom H -H2 mem_fdom domE.
+    smt ().
    wp; skip; rewrite /inv /= /#.
   wp; skip; rewrite /inv /#.
 + by auto => />.
diff --git a/theories/crypto/assumptions/PKSMK.ec b/theories/crypto/assumptions/PKSMK.ec
index 15cd538744..af636be0b7 100644
--- a/theories/crypto/assumptions/PKSMK.ec
+++ b/theories/crypto/assumptions/PKSMK.ec
@@ -251,10 +251,8 @@ section.
              ={glob RealSigServ, glob OrclUF} /\ 
                valid RealSigServ.pks_sks{1} RealSigServ.qs{1},
              ={OrclUF.forged}).
-    + by conseq |>; proc; sp; if; 
-         1: (by move => *; progress => /#);
-         by auto => />; smt(get_setE).
-    +  move => ??; conseq |>; proc; sp; if; auto => />; smt(keygen_ll). 
+    + by conseq |>; proc; sp; if=> [/>||]; auto=> />; smt(get_setE).
+    + by move => ??; conseq |>; proc; sp; if; auto => />; smt(keygen_ll). 
     + by move => ?; conseq |>; proc; sp; if; auto => />; smt(keygen_ll). 
     + conseq |>; proc; sp; if; 1: smt().
         if;
@@ -651,7 +649,7 @@ abstract theory UF1_UF.
         by smt(emptyE get_setE).
       + proc; inline *;auto => /> &m1 &m2 hpki _ h _.
         case (MkAdvUF1.mpki{m2}.[MkAdvUF1.pki{m2}] = Some MkAdvUF1.i{m2}) => h1.
-        + by apply fsetP => pk;rewrite in_fsetU in_fset1 !mem_fdom /#.
+        + by apply: fsetP=> pk; rewrite in_fsetU in_fset1 !mem_fdom !domE /#.
         by apply fsetP => pk;rewrite !mem_fdom /#.
       + proc;if => //; inline *; auto => /> &m1 &m2 hpki _ hpks hforge hpk. 
         rewrite /is_forgery; have := hpks pk{m2}; rewrite hpk /= /dom => -[->> ->] /=.
diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca
index 35bab15c69..435ecbadcf 100644
--- a/theories/crypto/prp_prf/Strong_RP_RF.eca
+++ b/theories/crypto/prp_prf/Strong_RP_RF.eca
@@ -145,7 +145,9 @@ proc; seq  1: (exists x, support uD x /\ !X x)=> //=.
 if=> //=.
 + rnd (predT); skip.
   move=> /> &0; rewrite dexceptedE predTI mu_not.
-  smt(notin_supportIP).
+  move=> x x_in_uD x_notin_X r_in_X.
+  apply/mulrV/ltr0_neq0/subr_gt0/notin_supportIP.
+  by exists x.
 by hoare; rnd=> //=; skip=> &hr ->.
 qed.
 
@@ -473,7 +475,9 @@ section CollisionProbability.
         + by apply/fun_ext=> x; rewrite mem_frng.
         apply/mu_mem_le; move=> x _; have [] uD_suf [] _ uD_fu:= uD_uf_fu.
         apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //.
-        smt(RealOrder.ler_wpmul2r mu_bounded le_fromint ltrW leq_card_rng_dom).
+        apply: RealOrder.ler_wpmul2r.
+        + exact: ge0_mu.
+        + exact/le_fromint/(lez_trans _ _ _ (leq_card_rng_dom _)).
       - by move: H9; rewrite H1.
     * by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
   + move=> c; proc; rcondt 2; 1:by auto.
diff --git a/theories/datatypes/List.ec b/theories/datatypes/List.ec
index ee56c61918..4e04fd5c4a 100644
--- a/theories/datatypes/List.ec
+++ b/theories/datatypes/List.ec
@@ -1633,7 +1633,15 @@ qed.
 
 lemma index_uniq z0 i (s : 'a list):
   0 <= i < size s => uniq s => index (nth z0 s i) s = i.
-proof. by elim: s i=> //=; smt(mem_nth). qed.
+proof.
+elim: s i=> //= [/#|x s ih i [] ge0_i].
+rewrite addzC=> /ltzS /lez_eqVlt le_i_sizeS.
+move=> [] x_notin_s uniq_s.
+case: (i = 0)=> /> i_neq_0.
+rewrite index_cons; case: (nth z0 s (i - 1) = x)=> [/>|_].
++ by move: x_notin_s; apply: contraLR=> _ /=; apply: mem_nth=> /#.
+by rewrite ih // /#.
+qed.
 
 lemma nth_uniq (s : 'a list) :
   (forall (i j : int), 0 <= i < size s => 0 <= j < size s => i <> j =>
@@ -1699,7 +1707,9 @@ qed.
 lemma uniq_le_perm_eq (s1 s2 : 'a list) :
   uniq s1 => mem s1 <= mem s2 => size s2 <= size s1 => perm_eq s1 s2.
 proof.
-  elim: s1 s2 => [| x l ih s2 /= [ninl uql] lemem le1sz]; 1: smt(size_ge0).
+  elim: s1 s2 => [| x l ih s2 /= [ninl uql] lemem le1sz].
+  + move=> s _ _ /= le0_size_s.
+    have -> //: s = [] by smt(size_ge0).
   move: (ih (rem x s2) uql _ _); 1,2: smt(mem_rem_neq size_rem).
   rewrite -(perm_cons x) => pxc; rewrite (perm_eq_trans _ _ _ pxc).
   by rewrite perm_eq_sym perm_to_rem /#.
@@ -2111,7 +2121,14 @@ proof. exact: nth_mapi_rec. qed.
 lemma mapi_recP x0 (f : int -> 'a -> 'b) (s : 'a list) y m :
     y \in mapi_rec f s m <=>
     exists n, (0 <= n && n < size s) /\ y = f (n+m) (nth x0 s n).
-proof. elim: s m; smt(size_ge0). qed.
+proof.
+elim: s m; 1:smt(size_ge0).
+move=> x xs ih m /=; case: (y = f m x)=> [/>|/= y_neq_fmx].
++ by exists 0; smt(size_ge0).
+rewrite ih; split.
++ by move=> [] n hn; exists (n + 1)=> /#.
++ by move=> [] n hn; exists (n - 1)=> /#.
+qed.
 
 lemma mapiP x0 (f : int -> 'a -> 'b) (s : 'a list) y :
     y \in mapi f s <=>
@@ -3800,13 +3817,23 @@ end section ListMax.
 lemma maxr_seq (f : 'a -> real) (s : 'a list) x0 :
   x0 \in s => exists x, x \in s /\ forall y, y \in s => f y <= f x.
 proof.
-by case: s => // x s _; elim: s x => {x0} [|y s IHs] x; smt().
+case: s => // x s _; elim: s x => {x0} [|y s IHs] x.
++ by exists x.
+case: (forall z, z = y \/ z \in s => f z <= f x).
++ by move=> z_is_min; exists x=> /#.
+move: (IHs y)=> - [] x1 /= hx1 x_not_max.
+by exists x1=> /#.
 qed.
 
 lemma maxz_seq (f : 'a -> int) (s : 'a list) x0 :
   x0 \in s => exists x, x \in s /\ forall y, y \in s => f y <= f x.
 proof.
-by case: s => // x s _; elim: s x => {x0} [|y s IHs] x; smt().
+case: s => // x s _; elim: s x => {x0} [|y s IHs] x.
++ by exists x.
+case: (forall z, z = y \/ z \in s => f z <= f x).
++ by move=> z_is_min; exists x=> /#.
+move: (IHs y)=> - [] x1 /= hx1 x_not_max.
+by exists x1=> /#.
 qed.
 
 (* -------------------------------------------------------------------- *)
diff --git a/theories/datatypes/MSet.ec b/theories/datatypes/MSet.ec
index 1c415b36c0..ff290e40e8 100644
--- a/theories/datatypes/MSet.ec
+++ b/theories/datatypes/MSet.ec
@@ -137,7 +137,8 @@ case (exists a, a \in m /\ nseq (oget m.[a]) a = nseq v k) =>
     subst e; rewrite get_set_sameE k_in /= lez_maxl // lez_maxl //.
   rewrite lP.
   split => [[a [/mem_set [a_in|->] ->]]|[a [a_in ->]]].
-  + by exists a; rewrite a_in /= get_set_neqE 1:/#. 
+  + exists a; rewrite a_in /= get_set_neqE //.
+    by rewrite -negP=> ->>; move: a_in; rewrite domE k_in.
   + by exists x; rewrite x_in /= get_set_sameE eq_nseq.
   have a_neq: a <> k.
   + rewrite -negP => a_eq; subst a.
@@ -309,7 +310,10 @@ qed.
 (* -------------------------------------------------------------------- *)
 lemma eqEsubset (s1 s2 : 'a mset) : 
   (s1 = s2) <=> (s1 \subset s2) /\ (s2 \subset s1).
-proof. smt(mset_eqP). qed.
+proof.
+split=> // - [] s1_sub_s2 s2_sub_s1.
+by apply: mset_eqP=> /#.
+qed.
 
 lemma subset_msetU_id (A B : 'a mset) :
   A \subset B => A `|` B = B.
diff --git a/theories/datatypes/Word.eca b/theories/datatypes/Word.eca
index 07582d5a47..60e2b6ffc7 100644
--- a/theories/datatypes/Word.eca
+++ b/theories/datatypes/Word.eca
@@ -30,7 +30,12 @@ proof. smt(valK). qed.
 lemma ofwordK :
   forall (s : t list), size s = n =>
     ofword (mkword s) = s.
-proof. smt(insubT). qed.
+proof.
+move=> s size_s. rewrite /ofword /mkword.
+have ->: odflt (insubd wordw) (insub s) = insubd s.
++ by move: (insubP s); rewrite {2}/insubd size_s=> /= - [] w [] ->.
+exact: insubdK.
+qed.
 
 lemma mkword_out :
   forall (s : t list), size s <> n =>
diff --git a/theories/datatypes/Xreal.ec b/theories/datatypes/Xreal.ec
index e2fac68d6d..a395b40172 100644
--- a/theories/datatypes/Xreal.ec
+++ b/theories/datatypes/Xreal.ec
@@ -64,12 +64,23 @@ theory Rp.
 
 subtype realp = { x : real | 0.0 <= x }
   rename "of_real", "to_real".
-
 realize inhabited by exists 0%r.
 
 abbrev (%r) = to_real.
 abbrev (%rp) = of_reald.
 
+lemma of_realKd_ge0 (x : real): 0%r <= x => x%rp%r = x.
+proof. smt(of_realdK to_realP). qed.
+
+lemma of_reald_pinj (x y:real):
+  0%r <= x => 0%r <= y => x%rp = y%rp => x = y.
+proof.
+move=> ge0_x ge0_y.
+move: (of_realP x); rewrite ge0_x=> /= - [] xp [] xpP <-.
+move: (of_realP y); rewrite ge0_y=> /= - [] yp [] ypP <-.
+by rewrite !to_realKd.
+qed.
+
 theory IntNotation.
   abbrev (%rp) (n:int) = n%r%rp.
 end IntNotation. export IntNotation.
@@ -99,13 +110,70 @@ abbrev (/) (x y : realp) : realp = x * inv y.
 abbrev (<=) (x y : realp) = x%r <= y%r.
 abbrev (<) (x y : realp)  = x%r < y%r.
 
+lemma addrpA: associative Rp.(+).
+proof.
+move=> x y z; rewrite /(+).
+congr; rewrite !of_realKd_ge0 ?addr_ge0 //.
+exact: RField.addrA.
+qed.
+
+lemma addrpC: commutative Rp.(+).
+proof.
+move=> x y; rewrite /(+).
+by congr; exact: RField.addrC.
+qed.
+
+lemma add0rp: left_id 0%rp (+).
+proof. done. qed.
+
+lemma mulrpA: associative Rp.( * ).
+proof.
+move=> x y z; rewrite /( * ).
+congr; rewrite !of_realKd_ge0 ?mulr_ge0 //.
+exact: RField.mulrA.
+qed.
+
+lemma mulrpC: commutative Rp.( * ).
+proof.
+move=> x y; rewrite /( * ).
+by congr; exact: RField.mulrC.
+qed.
+
+lemma mul1rp: left_id 1%rp Rp.( * ).
+proof. done. qed.
+
+lemma one_neq0_rp: 1%rp <> 0%rp.
+proof. by rewrite -negP=> eq_10; move: (of_reald_pinj 1%r 0%r _ _). qed.
+
+lemma mulrpDl: left_distributive Rp.( * ) Rp.(+).
+proof.
+move=> x y z; rewrite /(+) /( * ).
+congr; rewrite !of_realKd_ge0 ?(addr_ge0, mulr_ge0) //.
+by rewrite RField.mulrDl.
+qed.
+
+lemma addrpI: right_injective Rp.(+).
+proof.
+move=> x y y'; rewrite /(+)=> /(congr1 to_real).
+rewrite !of_realKd_ge0 ?addr_ge0 //.
+by move=> /RField.addrI/to_real_inj.
+qed.
 clone include MonoidDI with
    type t  <- realp,
    op zero <- of_reald 0.0,
    op MulMonoid.one  <- of_reald 1.0,
    op ( + ) <- Rp.( + ),
-   op ( * ) <- Rp.( * )
-proof * by smt(of_realdK to_realP to_real_inj).
+   op ( * ) <- Rp.( * ),
+   lemma Axioms.addmA <- addrpA,
+   lemma Axioms.addmC <- addrpC,
+   lemma Axioms.add0m <- add0rp,
+   lemma MulMonoid.Axioms.mulmA <- mulrpA,
+   lemma MulMonoid.Axioms.mulmC <- mulrpC,
+   lemma MulMonoid.Axioms.mul1m <- mul1rp,
+   lemma one_neq0 <- one_neq0_rp,
+   lemma mulmDl <- mulrpDl,
+   lemma addmI <- addrpI
+proof *.
 
 lemma to_realD (x y:realp) : (x + y)%r = x%r + y%r.
 proof. smt (of_realdK to_realP). qed.
@@ -250,7 +318,7 @@ realize MulMonoid.Axioms.mulmA by move=> [x|] [y|] [z|] //=; apply Rp.MulMonoid.
 realize MulMonoid.Axioms.mulmC by move=> [x|] [y|] //=; apply Rp.MulMonoid.mulmC.
 realize MulMonoid.Axioms.mul1m by move=> [x|] //=; apply Rp.MulMonoid.mul0m.
 realize one_neq0 by apply/negP => /(congr1 to_real).
-realize mulmDl by move=> [x|] [y|] [z|] //=; apply Rp.mulmDl.
+realize mulmDl by move=> [x|] [y|] [z|] //=; apply Rp.mulrpDl.
 
 (* -------------------------------------------------------------- *)
 lemma xaddxoo x : x + oo = oo.
@@ -666,8 +734,9 @@ proof.
   rewrite /psuminf => h hg.
   case: (summable (to_real g)) => // hgs.
   have h1 : forall (x : 'a), 0%r <= to_real f x && to_real f x <= to_real g x by smt(Rp.to_realP).
-  have -> /= := summable_le_pos (to_real f) (to_real g) hgs h1. 
-  have /# := ler_sum_pos (to_real f) (to_real g) h1 hgs.
+  have -> /= := summable_le_pos (to_real f) (to_real g) hgs h1.
+  have:= ler_sum_pos (to_real f) (to_real g) h1 hgs.
+  exact: le_pos.
 qed.
 
 lemma eq_Ep ['a] (d : 'a distr) (f g : 'a -> xreal) :
@@ -946,7 +1015,7 @@ proof. by move=> h;apply xle_cxr => />. qed.
 
 (* TODO: move this *)
 lemma Rp_to_real_eq (x y : realp) : (x = y) <=> (to_real x = to_real y).
-proof. smt(to_realKd). qed.
+proof. by split=> [/>|/to_real_inj]. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma Ep_cxr (d:'a distr) (b:'a -> bool) (f:'a -> xreal) : 
diff --git a/theories/distributions/DInterval.ec b/theories/distributions/DInterval.ec
index 66f284d460..8b93983e7a 100644
--- a/theories/distributions/DInterval.ec
+++ b/theories/distributions/DInterval.ec
@@ -75,7 +75,7 @@ have uniq_s: uniq s; first apply: uniq_flatten_map.
 have mem_s: forall x, (x \in s) <=> (x \in range 0 p).
 - move=> x; rewrite mem_range; split.
   - case/flatten_mapP=> j [/= /mem_range rgj] /=.
-    case/mapP => [k [/mem_range rgk]] ->; split; smt(@IntDiv).
+    case/mapP => [k [/mem_range rgk]] ->; split; [smt()|smt(@IntDiv)].
   - case=> ge0x lex; apply/flatten_mapP => /=.
     exists (x %/ q); rewrite mem_range.
     rewrite divz_ge0 // ge0x /=; split; 1: smt(@IntDiv).
diff --git a/theories/distributions/DList.ec b/theories/distributions/DList.ec
index 45b11bcc4c..c5daa724db 100644
--- a/theories/distributions/DList.ec
+++ b/theories/distributions/DList.ec
@@ -185,7 +185,10 @@ case (n < 0)=> [Hlt0 Hu xs ys| /lezNgt Hge0 Hu xs ys].
 rewrite !supp_dlist // => -[eqxs Hxs] [eqys Hys].
 rewrite !dlist1E // eqxs eqys /=;move: eqys;rewrite -eqxs => {eqxs}.
 elim: xs ys Hxs Hys => [ | x xs Hrec] [ | y ys] //=; 1,2:smt (size_ge0).
-rewrite !big_consT /#.
+rewrite !big_consT.
+move=> /= /> x_in_d all_in_d_xs y_in_d all_in_d_ys /addzI eq_size.
+rewrite (Hrec ys) //.
+by congr=> //; exact: Hu.
 qed.
 
 lemma dlist_dmap ['a 'b] (d : 'a distr) (f : 'a -> 'b) n :
@@ -199,7 +202,9 @@ qed.
 lemma dlist_rev (d:'a distr) n s:
   mu1 (dlist d n) (rev s) =  mu1 (dlist d n) s.
 proof.
-case (n <= 0) => [?|?]; first by rewrite !dlist0E //; 1:smt(revK).
+case (n <= 0) => [?|?].
++ rewrite !dlist0E // /pred1 /= -{1}rev_nil.
+  by congr; rewrite eq_iff; split=> />; exact: rev_inj.
 case (size s = n) => [<-|?]; 2: smt(dlist1E supp_dlist_size size_rev).
 by rewrite -{1}size_rev &(dlist_perm_eq) perm_eq_sym perm_eq_rev.
 qed.
diff --git a/theories/distributions/Distr.ec b/theories/distributions/Distr.ec
index 1b803058da..cd368df1dc 100644
--- a/theories/distributions/Distr.ec
+++ b/theories/distributions/Distr.ec
@@ -516,20 +516,20 @@ qed.
 op p_max (p: 'a distr) = flub (mu1 p).
 
 lemma has_fub_mu1 (d: 'a distr) : has_fub (mu1 d).
-proof. by apply (@ler_has_fub _ (fun _ => 1%r)) => // /#. qed.
+proof. by apply: (@ler_has_fub _ (fun _=> 1%r))=> //; exists 1%r. qed.
 
 lemma pmax_ge0 (p: 'a distr) :
   0%r <= p_max p.
 proof.
 suff: mu1 p witness <= p_max p by smt(ge0_mu).
-apply (@flub_upper_bound (mu1 p)); smt(le1_mu).
+by apply: (@flub_upper_bound (mu1 p)); exists 1%r; smt(le1_mu).
 qed.
 
 lemma pmax_gt0 (p: 'a distr) x :
   x \in p => 0%r < p_max p.
 proof.
 move => in_xp; suff: p_max p >= mu1 p x by smt(ge0_mu).
-apply (@flub_upper_bound (mu1 p)); smt(le1_mu).
+apply: (@flub_upper_bound (mu1 p)); exists 1%r; smt(le1_mu).
 qed.
 
 lemma pmax_le1 (p: 'a distr) :
@@ -554,9 +554,11 @@ move => unif_d; apply eqr_le; split.
   apply divr_ge0; first exact ge0_weight.
   smt(size_ge0).
 - move => _; case (weight d = 0%r) => ?; first by smt(pmax_ge0).
-  have [x in_xd]: exists x, x \in d by smt(witness_support ge0_mu).
+  have [x in_xd]: exists x, x \in d.
+  + move: (witness_support predT d)=> /iffLR /(_ _); 1:smt(ge0_mu).
+    by rewrite /predT.
   have <-: mu1 d x = weight d / (size (to_seq (support d)))%r by smt(mu1_uni).
-  apply (@flub_upper_bound (mu1 d)) => /=; smt(le1_mu).
+  by apply: (@flub_upper_bound (mu1 d)) => /=; exists 1%r; smt(le1_mu).
 qed.
 
 (* -------------------------------------------------------------------- *)
@@ -1536,7 +1538,8 @@ lemma dscale_uni ['a] (d : 'a distr) :
 proof.
 case: (weight d = 0%r) => Hw.
 + by move=> _ x y _ _; rewrite !dscale1E Hw.
-apply dscalar_uni =>//; smt (ge0_weight @Real).
+apply: dscalar_uni=> //; split=> //.
+by apply: invr_gt0; smt(ge0_mu).
 qed.
 
 (* -------------------------------------------------------------------- *)
@@ -2435,9 +2438,9 @@ qed.
 lemma dfun_unit (f : t -> 'u) : dfun (fun x => dunit (f x)) = dunit f. 
 proof.
 apply eq_distr => g; rewrite dunit1E dfun1E /=.
-case (f = g) => [<- | ?].
+case (f = g) => [<- | f_neq_g].
 + by rewrite BRM.big1 // => x _ /=; rewrite dunit1E.
-have [x hx]: exists x, f x <> g x by smt(). 
+move: f_neq_g; rewrite fun_ext negb_forall=> /= - [x hx].
 by rewrite (@BRM.bigD1 _ _ x) 1:FinT.enumP 1:FinT.enum_uniq /= dunit1E hx.
 qed.
 
@@ -2836,7 +2839,7 @@ proof.
 rewrite /hasE => Edf.
 apply (@summable_le (fun x => inv (mu d p) * (f x * mu1 d x))) => [|x /=].
 - exact/summableZ.
-- rewrite dcond1E /#.
+- by rewrite dcond1E; case: (p x)=> /#.
 qed.
 
 (* -------------------------------------------------------------------- *)
diff --git a/theories/distributions/Mu_mem.ec b/theories/distributions/Mu_mem.ec
index 226f3fc7c0..b65d5f9103 100644
--- a/theories/distributions/Mu_mem.ec
+++ b/theories/distributions/Mu_mem.ec
@@ -101,7 +101,14 @@ proof.
 elim/fmapW : m; first by rewrite mu0_false; smt(mem_empty fsize_empty).
 move => m k v fresh_k IH H.
 rewrite (@mu_eq _ _ (predU (p k)
-  (fun (r : 'c) => exists (u : 'a), (u \in m) /\ p u r))); 1: smt(mem_set).
+  (fun (r : 'c) => exists (u : 'a), (u \in m) /\ p u r))).
++ move=> x; rewrite /predU /= eq_iff exists_orl /=; split.
+  + move=> [] u; rewrite mem_set=> - [] [].
+    + by move=> u_in_m pu_x; exists u; right.
+    + by move=> />.
+  + move=> [] u [].
+    + by move=> pk_x; exists k; rewrite mem_set.
+    + by move=> [] u_in_m pu_x; exists u; rewrite mem_set u_in_m pu_x.
 rewrite mu_or; apply ler_naddr; 1: smt(mu_bounded).
 by rewrite fsize_set -mem_fdom fresh_k fromintD mulrDl; smt(mem_set).
 qed.
diff --git a/theories/distributions/SDist.ec b/theories/distributions/SDist.ec
index b3cbece743..086147e842 100644
--- a/theories/distributions/SDist.ec
+++ b/theories/distributions/SDist.ec
@@ -147,8 +147,9 @@ suff : maxr SEp (-SEn) <= Sp by smt().
 apply/ler_maxrP; split. 
 - (apply ler_sum; 1: smt()); 2: exact/summable_cond.
   exact/summable_cond/norm_summable/summable_sdist.
-- apply: ler_trans ler_Sn_Sp; 
-    rewrite -sumN; (apply ler_sum; 1: smt()); 2: exact/summable_cond.
+- apply: ler_trans ler_Sn_Sp.
+  rewrite -sumN.
+  apply: ler_sum; [1:by move=> @/predI @/predC /#|3:exact:summable_cond].
   exact/summableN/summable_cond/norm_summable/summable_sdist.
 qed.
 
@@ -172,8 +173,12 @@ pose Sp := sum (fun (x : 'a) =>
            if p x then (mu1 d1 x - mu1 d2 x) * mu (F x) E else 0%r).
 pose Sn := sum (fun (x : 'a) => 
            if !p x then (mu1 d1 x - mu1 d2 x) * mu (F x) E else 0%r).
-have Sp_ge0 : 0%r <= Sp by apply ge0_sum => /= x;smt(mu_bounded).
-have Sn_le0 : Sn <= 0%r by apply le0_sum => /= x;smt(mu_bounded).
+have Sp_ge0 : 0%r <= Sp.
++ apply: ge0_sum => /= x; case: (p x)=> /> @/p px.
+  by apply/mulr_ge0; [exact: subr_ge0 | exact: ge0_mu].
+have Sn_le0 : Sn <= 0%r.
++ apply: le0_sum=> /= x; case: (p x)=> /> @/p /ltrNge px.
+  by apply: nmulr_rle0; [exact:subr_lt0 | exact: ge0_mu].
 case : (`|Sp| >= `|Sn|) => H.
 + apply (ler_trans (2%r*Sp)); 1: smt().
   apply (ler_trans (2%r * sum (fun x => if p x then mu1 d1 x - mu1 d2 x else 0%r))).
diff --git a/theories/encryption/Hybrid.ec b/theories/encryption/Hybrid.ec
index 146a20be30..1124a4f13f 100644
--- a/theories/encryption/Hybrid.ec
+++ b/theories/encryption/Hybrid.ec
@@ -427,7 +427,8 @@ section.
     rewrite is_finiteE; exists (range 0 q).
     by rewrite range_uniq=> /= x; rewrite mem_range supp_dinter=> /#.
   have Huni : forall (x : int), x \in [0..max 0 (q - 1)] => mu1 [0..max 0 (q - 1)] x = 1%r / q%r.
-    by move=> x Hx; rewrite dinter1E /=; smt(supp_dinter).
+  + move=> x hx; rewrite dinter1E /=.
+    by rewrite -supp_dinter hx /= /#.
   pose ev :=
     fun (_j:int) (g:glob HybGameFixed(L(Ob))) (r:outputA),
       let (ga,ge,l,l0) = g in p ga ge l r /\ l <= q.