diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec
index 99ec64cb28..c3383a5f03 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 (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..cca8f6031b 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.
@@ -302,6 +308,22 @@ move=> eq; rewrite ltrNge /= ler_eqVlt; left.
 by apply/eq_sym; apply: inj_rexpr eq => /#.
 qed.
 
+lemma rpow_mono_base_ge1 (x n m : real) :
+  1%r <= x => n <= m => x ^ n <= x ^ m.
+proof.
+move => ??.
+case (n < 0%r) => ?.
+- case (m < 0%r) => ?.
+  - rewrite (: n = - - n) // (: m = - - m) //.
+    rewrite rpowN 1:/# (rpowN _ (-m)) 1:/#.
+    by rewrite RealOrder.ler_pinv 1,2,3,4:#smt:(rpow_gt0) &(rexpr_hmono) /#.
+  - apply (RealOrder.ler_trans 1%r).
+    - rewrite (: n = - - n) // -RField.invr1 -(rpow0 x) rpowN 1:/#.
+      by rewrite RealOrder.ler_pinv 1,2,3,4:#smt:(rpow_gt0) &(rexpr_hmono) /#.
+    - by rewrite -(rpow0 x) &(rexpr_hmono) /#.
+- by rewrite &(rexpr_hmono) /#.
+qed.
+
 (* -------------------------------------------------------------------- *)
 lemma le1Dx_rpowe (x : real): 0%r <= x => 1%r+x <= e^x.
 proof. by rewrite rpoweE; apply/le1Dx_exp. qed.
diff --git a/theories/core/Core.ec b/theories/core/Core.ec
index 80b59fc30d..86af58f0b9 100644
--- a/theories/core/Core.ec
+++ b/theories/core/Core.ec
@@ -1,3 +1,4 @@
+
 (* -------------------------------------------------------------------- *)
 lemma pw_eq ['a 'b] (x x' : 'a) (y y' : 'b):
   x = x' => y = y' => (x, y) = (x', y').
@@ -15,8 +16,8 @@ proof. by done. qed.
 
 lemma oget_some (x : 'a): oget (Some x) = x.
 proof. by done. qed.
-hint simplify oget_some, oget_none.
 
+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 +33,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 oget_ext ['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..c542bd250a 100644
--- a/theories/datatypes/Int.ec
+++ b/theories/datatypes/Int.ec
@@ -378,3 +378,7 @@ 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.
diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec
index 725160d0ca..2f89139c8c 100644
--- a/theories/prelude/Logic.ec
+++ b/theories/prelude/Logic.ec
@@ -365,12 +365,24 @@ 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 (x y z : bool) :
+  (x <=> y) => (y <=> z) => (x <=> z).
+proof. by smt(). qed.
+
 (* -------------------------------------------------------------------- *)
 lemma if_congr ['a] (e e' : bool) (c1 c2 c1' c2': 'a) :
      e = e' => c1 = c1' => c2 = c2'