diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec
index 99ec64cb28..41fd91356a 100644
--- a/theories/algebra/Ring.ec
+++ b/theories/algebra/Ring.ec
@@ -469,6 +469,9 @@ abstract theory ComRing.
   lemma expr1 x: exp x 1 = x.
   proof. by rewrite /exp /= iterop1. qed.
 
+  lemma exprE_ge0 (x : t) n : 0 <= n => exp x n = iter n (( * ) x) oner.
+  proof. by move=> ge0_n; rewrite /exp ltzNge ge0_n /= MulMonoid.iteropE. qed.
+
   lemma exprS (x : t) i: 0 <= i => exp x (i+1) = x * (exp x i).
   proof.
     move=> ge0i; rewrite /exp !ltzNge ge0i addz_ge0 //=.
diff --git a/theories/analysis/RealExp.ec b/theories/analysis/RealExp.ec
index b99a51e998..43561d22b0 100644
--- a/theories/analysis/RealExp.ec
+++ b/theories/analysis/RealExp.ec
@@ -61,6 +61,9 @@ apply/(mulfI _ (exp_neq0 x)); rewrite -expD addrN exp0.
 by rewrite mulrV // exp_neq0.
 qed.
 
+lemma expB (x y : real) : exp (x - y) = exp x / exp y.
+proof. by rewrite expD expN. qed.
+
 lemma exp_mono_ltr (x y : real): (exp x < exp y) <=> (x < y).
 proof. by apply/lerW_mono/exp_mono. qed.
 
@@ -159,6 +162,9 @@ proof. by move=> gt0x; rewrite !(rpowN, rpowD) // ltrW. qed.
 lemma rpowM (x n m : real) : 0%r < x => x^(n * m) = (x ^ n) ^ m.
 proof. by move=> gt0x; rewrite !rpowE ?exp_gt0 // lnK mulrCA mulrA. qed.
 
+lemma expM (x y : real) : exp (x * y) = (exp x) ^ y.
+proof. by rewrite rpowE 1:exp_gt0 lnK RField.mulrC. qed.
+
 lemma rpowMr (x y n : real) :
   0%r < x => 0%r < y => (x * y)^n = x^n * y^n.
 proof.
@@ -285,18 +291,34 @@ move=> gt0_x ne1_x; rewrite !rpowE // => /inj_exp.
 by apply: mulIf; rewrite ln_eq0.
 qed.
 
-lemma rexpr_hmono (x n m : real) :
+lemma rexpr_ge0_hmono_ltr (x n m : real) :
   1%r <= x => 0%r <= n <= m => x^n <= x^m.
 proof.
-move=> ge1x [ge0n lenm]; have ge0m: 0%r <= m by apply/(ler_trans n).
+move=> ge1x [ge0n lenm];
+  have ge0m: 0%r <= m by apply/(ler_trans n).
 rewrite !rpowE 1,2:(ltr_le_trans 1%r) // exp_mono.
 by apply/ler_wpmul2r=> //; apply/ln_ge0.
 qed.
 
+lemma rexprn_ege1 (x : real) (n : real) :
+  0%r <= n => 1%r <= x => 1%r <= x^n.
+proof.
+move=> ge0_n ge1_x; rewrite -[1%r](rpow0 x).
+by apply: rexpr_ge0_hmono_ltr.
+qed.
+
+lemma rexpr_hmono (x n m : real) :
+  1%r <= x => n <= m => x^n <= x^m.
+proof.
+move=> ge1_x le_nm; rewrite (_ : m = (m - n) + n) 1:#ring.
+rewrite rpowD 1:/# ler_pemull 1:rpow_ge0 1:/#.
+by rewrite (rexprn_ege1 x (m - n)) //#.
+qed.
+
 lemma rexpr_hmono_ltr (x n m : real) :
-  1%r < x => 0%r <= n < m => x^n < x^m.
+  1%r < x => n < m => x^n < x^m.
 proof.
-move=> gt0_x [gt0_n lt_nm]; rewrite ltr_neqAle.
+move=> gt0_x lt_nm; rewrite ltr_neqAle.
 rewrite rexpr_hmono ~-1://# /=; apply: contraL lt_nm.
 move=> eq; rewrite ltrNge /= ler_eqVlt; left.
 by apply/eq_sym; apply: inj_rexpr eq => /#.
@@ -331,7 +353,7 @@ rewrite -!(lt_fromint, le_fromint) => gt1_b ge1_x;
 - move=> @/ilog; rewrite -{1}(@rpowK b%r x%r) // 1:/#.
   rewrite -!fromintXn 1?(lez_trans (0+1)) //.
   - by rewrite ler_add2r ?ilog_ge0 /#.
-  rewrite -rpow_int // &(rexpr_hmono_ltr) // log_ge0 //= 1:/#.
+  rewrite -rpow_int // &(rexpr_hmono_ltr) //.
   by rewrite fromintD -ltr_subl_addr &(floor_gt).
 qed.
 
diff --git a/theories/core/Core.ec b/theories/core/Core.ec
index 80b59fc30d..21e3cf54df 100644
--- a/theories/core/Core.ec
+++ b/theories/core/Core.ec
@@ -17,7 +17,6 @@ lemma oget_some (x : 'a): oget (Some x) = x.
 proof. by done. qed.
 hint simplify oget_some, oget_none.
 
-
 lemma some_oget (x : 'a option): x <> None => x = Some (oget x).
 proof. by case: x. qed.
 
@@ -32,6 +31,13 @@ lemma oget_omap_some ['a 'b] (f : 'a -> 'b) ox :
   ox <> None => oget (omap f ox) = f (oget ox).
 proof. by case: ox. qed.
 
+lemma ogetI ['a] (x y : 'a option) :
+     x <> None
+  => y <> None
+  => oget x = oget y
+  => x = y.
+proof. by case x; case y. qed.
+
 (* -------------------------------------------------------------------- *)
 lemma frefl  (f     : 'a -> 'b): f == f by [].
 
diff --git a/theories/datatypes/Int.ec b/theories/datatypes/Int.ec
index ae26bbb6da..cf40d374ff 100644
--- a/theories/datatypes/Int.ec
+++ b/theories/datatypes/Int.ec
@@ -378,3 +378,11 @@ proof. by smt(). qed.
 
 lemma maxzz : idempotent max by smt().
 lemma minzz : idempotent min by smt().
+
+lemma lez_minP (w a b : int) :
+  w <= min a b <=> (w <= a /\ w <= b).
+proof. by smt(). qed.
+
+lemma gez_maxP (w a b : int) :
+  max a b <= w <=> (a <= w /\ b <= w).
+proof. by smt(). qed.
diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec
index 671c36d8f5..46a1df5dfa 100644
--- a/theories/prelude/Logic.ec
+++ b/theories/prelude/Logic.ec
@@ -2,7 +2,7 @@
 (* Run easycrypt via the commandline with a `-boot` flag instead        *)
 
 (* -------------------------------------------------------------------- *)
-require import Tactics.
+require import Tactics Pervasive.
 
 (* -------------------------------------------------------------------- *)
 abbrev [-printing] fst (p : 'a * 'b): 'a = p.`1.
@@ -364,12 +364,22 @@ lemma contraNneq (b : bool) (x y : 'a):
   (x = y => b) => !b => x <> y
 by smt().
 
+lemma contra_congr ['a 'b] (f : 'a -> 'b) (x y : 'a) :
+  f x <> f y => x <> y.
+proof. by rewrite &(contra) &(congr1). qed.
+
+(* -------------------------------------------------------------------- *)
+lemma case_elim p q: ((p => q) /\ (!p => q)) <=> q.
+proof. by smt(). qed.
+
 (* -------------------------------------------------------------------- *)
 lemma iffLR (a b : bool) : (a <=> b) => a => b by [].
 lemma iffRL (a b : bool) : (a <=> b) => b => a by [].
 
 lemma iff_negb : forall b1 b2, (!b1 <=> !b2) <=> (b1 <=> b2) by [].
 
+lemma iff_trans : transitive (<=>) by smt().
+
 (* -------------------------------------------------------------------- *)
 lemma if_congr ['a] (e e' : bool) (c1 c2 c1' c2': 'a) :
      e = e' => c1 = c1' => c2 = c2'