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..2c31166fd7 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.
@@ -286,17 +292,31 @@ by apply: mulIf; rewrite ln_eq0.
 qed.
 
 lemma rexpr_hmono (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).
-rewrite !rpowE 1,2:(ltr_le_trans 1%r) // exp_mono.
-by apply/ler_wpmul2r=> //; apply/ln_ge0.
+  1%r <= x => n <= m => x^n <= x^m.
+proof.
+move => ?.
+have Hnm : forall n' m', 0%r <= n' <= m' => x ^ n' <= x ^ m'.
++ move => n' m' [ge0n nlem].
+  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.
+move => ?.
+case (n < 0%r) => ?.
+- case (m < 0%r) => ?.
+  - rewrite (: n = - - n) // (: m = - - m) //.
+    rewrite rpowN 1:/# (rpowN _ (-m)) 1:/#.
+    rewrite RealOrder.ler_pinv 1,2,3,4:#smt:(rpow_gt0) &(Hnm) /#.
+  - 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) &(Hnm) /#.
+    - by rewrite -(rpow0 x) &(Hnm) /#.
+- by rewrite &(Hnm) /#.
 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 +351,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..10e949d9d1 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 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..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 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'