diff --git a/theories/algebra/IntDiv.ec b/theories/algebra/IntDiv.ec
index 742de63b14..970c7bdfa8 100644
--- a/theories/algebra/IntDiv.ec
+++ b/theories/algebra/IntDiv.ec
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-require import Core Int IntMin Ring StdOrder.
+require import Core Int IntMin Ring StdOrder List.
 (*---*) import Ring.IntID IntOrder.
 
 (* -------------------------------------------------------------------- *)
@@ -514,6 +514,14 @@ lemma nosmt eqz_mul d m n : d <> 0 => d %| m =>
   (m = n * d) <=> (m %/ d = n).
 proof. by move=> d_gt0 dv_d_m; rewrite eq_sym -eqz_div // eq_sym. qed.
 
+lemma divz_eqP (m d n : int) :
+  0 < d => m %/ d = n <=> n * d <= m < (n + 1) * d.
+proof.
+  move => lt0d; split => [<<-|[le_m ltm_]].
+  + by split => [|_]; [apply/lez_floor/gtr_eqF|apply/ltz_ceil].
+  by apply/eqz_leq; split; [apply/ltzS/ltz_divLR|apply/lez_divRL].
+qed.
+
 lemma nosmt leq_div2r (d m n : int) :
   m <= n => 0 <= d => m %/ d <= n %/ d.
 proof.
@@ -568,6 +576,47 @@ qed.
 lemma nosmt divzDr m n d : d %| n => (m + n) %/ d = (m %/ d) + (n %/ d).
 proof. by move=> dv_n; rewrite addrC divzDl // addrC. qed.
 
+lemma divz_mulp (n d1 d2 : int) : 
+  0 < d1 =>
+  0 < d2 =>
+  n %/ (d1 * d2) = n %/ d1 %/ d2.
+proof.
+  move => lt0d1 lt0d2; rewrite (mulzC d1); apply divz_eqP; [by apply mulr_gt0|split => [|_]].
+  + by rewrite mulrA; apply (lez_trans (n %/ d1 * d1));
+    [apply/ler_pmul2r => //|]; apply/lez_floor/gtr_eqF.
+  by rewrite mulrA; apply (ltr_le_trans ((n %/ d1 + 1) * d1));
+  [|apply/ler_pmul2r => //; apply/ltzE]; apply/ltz_ceil.
+qed.
+
+lemma divz_mul (n d1 d2 : int) :
+  0 <= d1 =>
+  n %/ (d1 * d2) = n %/ d1 %/ d2.
+proof.
+move => /lez_eqVlt [<<- //=|lt0d1];
+(case (0 <= d2) => [/lez_eqVlt [<<- //=|lt0d2]|/ltzNge ltd20]).
+(*FIXME: why no automatic rewriting here for divz0 and div0z?*)
++ by rewrite !divz0.
++ by rewrite !divz0 div0z.
++ by rewrite !divz0 div0z.
++ by rewrite !divz0.
++ by rewrite divz_mulp.
+by rewrite -(oppzK d2) mulrN 2!divzN eqr_opp divz_mulp // ltr_oppr.
+qed.
+
+lemma divzpMr p m d : d %| m => p * (m %/ d) = p * m %/ d.
+proof. by move => /dvdzP [q ->>]; case (d = 0) => [->> /=|neqd0]; [rewrite divz0|rewrite mulrA !mulzK]. qed.
+
+lemma dvdNdiv x y : x <> 0 => x %| y => (-y) %/ x = - y %/ x.
+proof. by move => neqx0 /dvdzP [z ->>]; rewrite -mulNr !mulzK. qed.
+
+lemma exprD_subz (x m n : int) : x <> 0 => 0 <= n <= m => x ^ (m - n) = (x ^ m) %/ (x ^ n).
+proof.
+move => neqx0 [le0n lenm]; rewrite eq_sym -(eqz_mul (x ^ n) (x ^ m) (x ^ (m - n))).
++ by move: neqx0; rewrite implybNN expf_eq0.
++ by apply dvdz_exp2l.
+by rewrite -exprD_nneg ?subrK // ler_subr_addr.
+qed.
+
 lemma nosmt expz_div (x n m : int) :
   0 <= m <= n => 0 < x => x^n %/ x^m = x^(n-m).
 proof.
@@ -856,6 +905,178 @@ move=> lt_pn; rewrite {1}(divz_eq i (k^n)); rewrite -addrA; congr.
 by rewrite {1}(divz_eq (i %% k^n) (k^p)) modz_dvd_pow.
 qed.
 
+lemma dvdz_mod_div d1 d2 m :
+  0 < d1 =>
+  0 < d2 =>
+  d2 %| d1 =>
+  m %% d1 %/ d2 = (m %/ d2) %% (d1 %/ d2).
+proof.
+  move => lt0d1 lt0d2 /dvdzP [q ->>]; rewrite modzE mulrA -mulNr mulzK; first by rewrite gtr_eqF.
+  rewrite divzMDr //; first by rewrite gtr_eqF.
+  rewrite addrC modzE; do 2!congr.
+  by rewrite (mulrC q) divz_mulp // -(pmulr_lgt0 _ _ lt0d2).
+qed.
+
+lemma modz_pow_div x n p m :
+  0 < x =>
+  0 <= p <= n =>
+  m %% x ^ n %/ x ^ p = (m %/ x ^ p) %% (x ^ (n - p)).
+proof.
+  by move => lt0x [le0p lepn]; rewrite dvdz_mod_div //;
+  [apply expr_gt0|apply expr_gt0|apply dvdz_exp2l|rewrite exprD_subz // gtr_eqF].
+qed.
+
+lemma modz_pow2_div n p m :
+  0 <= p <= n =>
+  m %% 2 ^ n %/ 2 ^ p = (m %/ 2 ^ p) %% (2 ^ (n - p)).
+proof. by apply modz_pow_div. qed.
+
+(* ==================================================================== *)
+lemma pow_normr (p x : int) :
+  p ^ x = p ^ `|x|.
+proof.
+by rewrite normE; case (0 <= x) => //; rewrite exprN. qed.
+
+lemma lt_pow (p x : int) :
+  1 < p =>
+  x < p ^ x.
+proof.
+  move => lt1p; case (0 <= x) => [|/ltzNge ltx0]; last by apply/(ltr_le_trans _ _ _ ltx0)/expr_ge0/ltzW/ltzE/ltzW.
+  elim x => [|x le0x ltxpow]; first by rewrite expr0.
+  apply/(ler_lt_trans (p ^ x)); first by apply/ltzE.
+  by rewrite exprSr // ltr_pmulr // expr_gt0 ltzE ltzW.
+qed.
+
+lemma Ndvd_pow (p x : int) :
+  1 < `|p| =>
+  x <> 0 =>
+  ! p ^ x %| x.
+proof.
+  move => lt1norm neqx0; apply/negP => dvdpowx.
+  move: (dvdz_le _ _ _ dvdpowx) => //.
+  rewrite pow_normr normrX_nat ?normr_ge0 //; apply/negP/ltzNge.
+  by apply/lt_pow.
+qed.
+
+lemma dvdz2_eq m n :
+  0 <= m =>
+  0 <= n =>
+  m %| n =>
+  n %| m =>
+  m = n.
+proof.
+  move => le0m le0n /dvdzP [x ->>] /dvdzP [y /(congr1 (transpose (%/) m) _ _) /=].
+  rewrite mulrA divzz; case (m = 0) => /= [->> //=|neqm0]. 
+  rewrite /b2i mulzK //= => eq1mul; move: (unitrM y x); move: eq1mul => <- /=.
+  move => [_ [|] ->> //=]; move: le0n; rewrite mulNr /= oppr_ge0 => lem0.
+  by move: neqm0; rewrite eqz_leq lem0 le0m.
+qed.
+
+lemma dvd_le_pow (p m n : int) :
+  1 < `|p| =>
+  p ^ m %| p ^ n =>
+  `|m| <= `|n|.
+proof.
+  rewrite (pow_normr p m) (pow_normr p n) => lt1norm dvdpow2.
+  have:= (dvdz_le _ _ _ dvdpow2); first by rewrite expf_eq0 -negP => -[_ ->>].
+  rewrite !normrX_nat ?normr_ge0 //.
+  by apply ler_weexpn2r => //; apply normr_ge0.
+qed.
+
+lemma le_dvd_pow (p m n : int) :
+  `|m| <= `|n| =>
+  p ^ m %| p ^ n.
+proof.
+  rewrite (pow_normr p m) (pow_normr p n) => lenormr2.
+  apply/dvdzP; exists (p ^ (`|n| - `|m|)).
+  by rewrite -exprD_nneg; [apply subr_ge0|apply normr_ge0|rewrite -addrA].
+qed.
+
+(*-----------------------------------------------------------------------------*)
+
+lemma eq_range m n : m = n <=> m \in range n (n+1).
+proof. by rewrite mem_range ltzS eqz_leq. qed.
+
+lemma range_div_range m d min max : 0 < d => m %/ d \in range min max <=> m \in range (min * d) (max * d).
+proof.
+move => lt0d; rewrite !mem_range !andabP; apply andb_id2.
++ by apply lez_divRL.
+by rewrite -ltz_divLR // ltzS.
+qed.
+
+lemma eq_div_range m d n : 0 < d => m %/ d = n <=> m \in range (n * d) ((n + 1) * d).
+proof. by move => lt0d; rewrite eq_range range_div_range. qed.
+
+(*-----------------------------------------------------------------------------*)
+abbrev (%\) (m d : int) : int = - ((- m) %/ d).
+
+lemma lez_ceil m d : d <> 0 => m <= m %\ d * d.
+proof. by rewrite mulNr => neqd0; apply/ler_oppr/lez_floor. qed.
+
+lemma ltz_floor m d : 0 < d => (m %\ d - 1) * d < m.
+proof. by rewrite -opprD mulNr => lt0d; apply/ltr_oppl/ltz_ceil. qed.
+
+lemma lez_NdivNLR (d m n : int) : 0 < d => d %| n => m <= n %\ d <=> m * d <= n.
+proof.
+move => lt0d dvddn; rewrite ler_oppr lez_divLR //; first by apply dvdzN.
+by rewrite mulNr ler_opp2.
+qed.
+
+lemma lez_NdivNRL (m n d : int) : 0 < d => m %\ d <= n <=> m <= n * d.
+proof. by move => lt0d; rewrite ler_oppl lez_divRL // mulNr ler_opp2. qed.
+
+lemma ltz_NdivNLR (m n d : int) : 0 < d => m < n %\ d <=> m * d < n.
+proof. by move => lt0d; rewrite ltr_oppr ltz_divLR // mulNr ltr_opp2. qed.
+
+lemma ltz_NdivNRL (d m n : int) : 0 < d => d %| m => m %\ d < n  <=> m < n * d.
+move => lt0d dvddm; rewrite ltr_oppl ltz_divRL //; first by apply dvdzN.
+by rewrite mulNr ltr_opp2.
+qed.
+
+(*-----------------------------------------------------------------------------*)
+
+lemma mem_range_mull (m n x y : int) :
+  0 < x =>
+  x * y \in range m n <=> y \in range (m %\ x) (n %\ x).
+proof. by move => lt0x; rewrite !mem_range lez_NdivNRL // ltz_NdivNLR // !(mulrC y). qed.
+
+lemma mem_range_mulr (m n x y : int) :
+  0 < y =>
+  x * y \in range m n <=> x \in range (m %\ y) (n %\ y).
+proof. by rewrite mulrC; apply/mem_range_mull. qed.
+
+lemma mem_range_mod (x y : int) :
+  y <> 0 =>
+  x %% y \in range 0 `|y|.
+proof. by move => neqy0; rewrite mem_range modz_ge0 // ltz_mod. qed.
+
+lemma mem_range_add_mul (m n l x y : int) :
+  x \in range 0 l =>
+  y \in range m n =>
+  x + l * y \in range (m * l) (n * l).
+proof.
+  move => Hx_range Hy_range; rewrite mem_range_addl mem_range_mull; first by apply/(ler_lt_trans x); move/mem_range: Hx_range.
+  move: Hy_range; apply/mem_range_incl.
+  + rewrite lez_NdivNRL; first by apply/(ler_lt_trans x); move/mem_range: Hx_range.
+    by rewrite ler_subl_addr ler_addl; move/mem_range: Hx_range.
+  rewrite -ltzS -ltr_subl_addr ltz_NdivNLR; first by apply/(ler_lt_trans x); move/mem_range: Hx_range.
+  by rewrite mulrDl mulNr /= ler_lt_sub //; move/mem_range: Hx_range.
+qed.
+
+lemma mem_range_add_mul_eq (x1 y1 x2 y2 l : int) :
+  x1 \in range 0 l =>
+  x2 \in range 0 l =>
+  x1 + l * y1 = x2 + l * y2 <=>
+  x1 = x2 /\ y1 = y2.
+proof.
+  move => /mem_range [le0x1 ltx1l] /mem_range [le0x2 ltx2l]; split => [Heq|[->> ->>] //]; split.
+  + move: (congr1 (transpose (%%)%IntID l) _ _ Heq) => /=.
+    by rewrite !(mulrC l) !modzMDr !pmod_small.
+  move: (congr1 (transpose (%/)%IntID l) _ _ Heq) => /=.
+  rewrite !(mulrC l) !divzMDr; try by apply/gtr_eqF/(ler_lt_trans x1).
+  by rewrite !pdiv_small.
+qed.
+
 lemma nosmt divzMr i a b :  
   0 <= a => 0 <= b => i %/ (a * b) = i %/ a %/ b.
 proof.
@@ -877,6 +1098,7 @@ lemma nosmt divzMl i a b :
   0 <= a => 0 <= b => i %/ (a * b) = i %/ b %/ a.
 proof. by move=> *; rewrite mulrC divzMr. qed.
 
+(*
 lemma nosmt modz_pow2_div n p i: 
   0 <= p <= n => (i %% 2^n) %/ 2^p = (i %/ 2^p) %% 2^(n-p).
 proof.
@@ -884,6 +1106,7 @@ move=> [ge0_p len_p].
 rewrite !modzE (: 2^n = 2^(n-p) * 2^p) 1:-exprD_nneg 1:subr_ge0 3:subrK //.
 by rewrite -mulNr mulrA divzMDr 1:expf_eq0 // mulNr addrC divzMl 1,2:expr_ge0.
 qed.
+*)
 
 (* -------------------------------------------------------------------- *)
 require import Real.
diff --git a/theories/algebra/Number.ec b/theories/algebra/Number.ec
index 41c7500261..31145de8f5 100644
--- a/theories/algebra/Number.ec
+++ b/theories/algebra/Number.ec
@@ -350,6 +350,25 @@ proof. by rewrite ltr_neqAle normr_le0 normr0P; case: (_ = _). qed.
 lemma nosmt normr_gt0 (x : t): (zeror < `|x|) <=> (x <> zeror).
 proof. by rewrite ltr_def normr0P normr_ge0; case: (_ = _). qed.
 
+lemma nosmt unit_normr (x : t): unit (`|x|) => unit x.
+proof.
+case: (real_axiom x) => [le0n|len0].
+  by move: (normr_idP x); rewrite le0n /= => ->.
+by rewrite ler0_norm // unitrN.
+qed.
+
+lemma nosmt normrX n (x : t) : `|exp x n| = exp `|x| n.
+proof.
+case (0 <= n); [by apply normrX_nat|].
+rewrite -ltzNge -{1}(invrK x) exprV => ltn0.
+rewrite normrX_nat; [by rewrite oppz_ge0 ltzW|].
+case: (unit x) => [unitx|Nunitx].
+  by rewrite normrV // exprV.
+move: (unit_normr x) => /contra; rewrite Nunitx /=.
+move => unitNx; rewrite invr_out //.
+by rewrite -{1}(@invr_out `|_|) // exprV.
+qed.
+
 (*-------------------------------------------------------------------- *)
 hint rewrite normrE : normr_id normr0 normr1 normrN1.
 hint rewrite normrE : normr_ge0 normr_lt0 normr_le0 normr_gt0.
@@ -729,7 +748,10 @@ proof. by rewrite ltrNge. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma leVge x y : (x <= y) \/ (y <= x).
-proof. by case: (x <= y) => // /ltrNge /ltrW. qed.
+proof. exact ler_total. qed.
+
+lemma leVgt x y : (x <= y) \/ (y < x).
+proof. by case: (x <= y) => // /ltrNge. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma nosmt ltrN10: -oner < zeror.
@@ -1099,6 +1121,14 @@ rewrite exprD_nneg 1:subz_ge0 // ler_pemull ?(expr_ge0, exprn_ege1) //.
 + by rewrite (@ler_trans oner). + by rewrite subz_ge0.
 qed.
 
+lemma ler_weexpn2r x : oner < x =>
+  forall m n, 0 <= m => 0 <= n => exp x m <= exp x n => m <= n.
+proof.
+move => lt1x m n le0m le0n; rewrite -implybNN -ltrNge -ltzNge ltzE => le_m; apply (ltr_le_trans (exp x (n + 1))).
++ by rewrite exprS //; apply ltr_pmull => //; apply/expr_gt0/(ler_lt_trans oner).
+by apply ler_weexpn2l; [apply ltrW|split => //; apply addz_ge0].
+qed.
+
 lemma nosmt ieexprn_weq1 x n : 0 <= n => zeror <= x =>
   (exp x n = oner) <=> (n = 0 || x = oner).
 proof.
@@ -1189,6 +1219,14 @@ proof. by rewrite ger0_def. qed.
 lemma nosmt eqr_normN (x : t): (`|x| = - x) <=> (x <= zeror).
 proof. by rewrite ler0_def. qed.
 
+lemma nosmt normE n :
+  `|n| = if zeror <= n then n else -n.
+proof.
+move: (real_axiom n); rewrite or_andr => -[le0n|[Nle0n len0]].
++ by rewrite le0n /= eqr_norm_id.
+by rewrite Nle0n /= eqr_normN.
+qed.
+
 (* -------------------------------------------------------------------- *)
 lemma ler_norm x : x <= `|x|.
 proof.
diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec
index 9037674793..0afada3062 100644
--- a/theories/algebra/Poly.ec
+++ b/theories/algebra/Poly.ec
@@ -1,6 +1,6 @@
 (* -------------------------------------------------------------------- *)
 require import AllCore Finite Distr DList List.
-require import Ring Bigalg StdBigop StdOrder.
+require import Ring IntMin Bigalg StdBigop StdOrder.
 require (*--*) Subtype.
 (*---*) import Bigint IntID IntOrder.
 
diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec
index e79679b382..8ff51e0cfd 100644
--- a/theories/algebra/Ring.ec
+++ b/theories/algebra/Ring.ec
@@ -235,6 +235,9 @@ abstract theory ComRing.
   lemma nosmt mulrACA: interchange ( * ) ( * ).
   proof. by move=> x y z t; rewrite -!mulrA (mulrCA y). qed.
 
+  lemma nosmt mulrSl x y : (x + oner) * y = x * y + y.
+  proof. by rewrite mulrDl mul1r. qed.
+
   lemma nosmt mulrDr: right_distributive ( * ) (+).
   proof. by move=> x y z; rewrite mulrC mulrDl !(@mulrC _ x). qed.
 
diff --git a/theories/algebra/StdOrder.ec b/theories/algebra/StdOrder.ec
index bff2baab82..76a890e4fe 100644
--- a/theories/algebra/StdOrder.ec
+++ b/theories/algebra/StdOrder.ec
@@ -71,6 +71,7 @@ move=> nz_0; rewrite b2i1 /= -{1}(mul1r `|z|); congr.
 rewrite -exprD_nneg ?b2i_ge0 -signr_odd ?addr_ge0 ?b2i_ge0.
 by rewrite -mul1r2z oddM /ofint_id intmulz odd2 expr0.
 qed.
+
 end IntOrder.
 
 (* -------------------------------------------------------------------- *)
diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec
index cfefa518c3..23dcbef6d9 100644
--- a/theories/algebra/ZModP.ec
+++ b/theories/algebra/ZModP.ec
@@ -22,7 +22,15 @@ op inzmod (z : int)  = Sub.insubd (z %% p).
 op asint  (z : zmod) = Sub.val z.
 
 lemma inzmodK (z : int): asint (inzmod z) = z %% p.
-proof. smt ml=1. qed.
+proof.
+rewrite /asint /inzmod Sub.insubdK //.
+rewrite modz_ge0 /= 1:&(gtr_eqF); first by smt(ge2_p).
+by apply: ltz_pmod; smt(ge2_p).
+qed.
+
+lemma inzmod_mod z :
+  inzmod z = inzmod (z %% p).
+proof. by rewrite /inzmod modz_mod. qed.
 
 lemma asint_inj: injective asint by apply/Sub.val_inj.
 
@@ -191,6 +199,23 @@ lemma inzmodB (a b : int):
   inzmod (a - b) = (inzmod a) + (- (inzmod b)).
 proof. by rewrite inzmodD inzmodN. qed.
 
+(* -------------------------------------------------------------------- *)
+lemma inzmodD_mod (a b : int):
+  inzmod ((a + b) %% p) = inzmod a + inzmod b.
+proof. by rewrite -inzmod_mod inzmodD. qed.
+
+lemma inzmodM_mod (a b : int):
+  inzmod ((a * b) %% p) = inzmod a * inzmod b.
+proof. by rewrite -inzmod_mod inzmodM. qed.
+
+lemma inzmodN_mod (n : int):
+  inzmod ((- n) %% p) = -(inzmod n).
+proof. by rewrite -inzmod_mod inzmodN. qed.
+
+lemma inzmodB_mod (a b : int):
+  inzmod ((a - b) %% p) = (inzmod a) + (- (inzmod b)).
+proof. by rewrite -inzmod_mod inzmodB. qed.
+
 (* -------------------------------------------------------------------- *)
 lemma intmul_asint (x : zmod) : x = intmul one (asint x).
 proof.
@@ -318,4 +343,101 @@ instance field with zmod
   proof expr0     by apply/ZModpField.expr0
   proof exprS     by apply/ZModpField.exprS
   proof exprN     by (move=> ?? _; apply/ZModpField.exprN).
+
+(* -------------------------------------------------------------------- *)
+lemma exp_inzmod m n :
+  exp (inzmod m) n =
+  if 0 <= n
+  then inzmod (exp m n)
+  else inv (inzmod (exp m (-n))).
+proof.
+  case: (0 <= n) => [|/ltzNge].
+  + elim: n => [|n le0n]; [by rewrite !expr0|].
+    by rewrite exprS // exprS // inzmodM => ->.
+  rewrite -oppr_gt0 => /ltzW le0Nn.
+  rewrite -(Ring.IntID.opprK n) exprN opprK.
+  apply congr1; move: (-n) le0Nn => {n} n.
+  elim n => [|n le0n]; [by rewrite !expr0|].
+  by rewrite exprS // exprS // inzmodM => ->.
+qed.
+
+lemma inzmod_exp (m n : int) :
+  inzmod (exp m n) =
+  if 0 <= n
+  then exp (inzmod m) n
+  else exp (inzmod m) (-n).
+proof.
+  move: (exp_inzmod m n); case: (0 <= n) => [_ -> //|/ltzNge ltn0].
+  by rewrite !exprN => ->; rewrite invrK.
+qed.
+
+lemma inzmod_exp_mod (m n k : int) :
+  inzmod (exp m k) = one =>
+  inzmod (exp m n) =
+  if 0 <= n
+  then inzmod (exp m (n %% k))
+  else inzmod (exp m ((-n) %% k)).
+proof.
+  case: (k = 0) => [->>|]; [by rewrite !modz0 exprN; case: (0 <= n)|].
+  rewrite -normr_gt0 pow_normr -modz_abs inzmod_exp normr_ge0 /=.
+  move => lt0normr eq_inzmod_one; case: (0 <= n) => [le0n|Nle0n].
+  + rewrite inzmod_exp le0n /= {1}(divz_eq n `|k|) exprD_nneg.
+    - by rewrite mulr_ge0; [rewrite divz_ge0|rewrite normr_ge0].
+    - by rewrite modz_ge0 gtr_eqF.
+    rewrite Ring.IntID.mulrC exprM eq_inzmod_one expr1z.
+    by rewrite mul1r exp_inzmod modz_ge0 // gtr_eqF.
+  move: Nle0n => /ltrNge; rewrite -exprN -oppr_gt0 => /ltzW le0Nn.
+  rewrite inzmod_exp le0Nn /= {1}(divz_eq (-n) `|k|) exprD_nneg.
+  + by rewrite mulr_ge0; [rewrite divz_ge0|rewrite normr_ge0].
+  + by rewrite modz_ge0 gtr_eqF.
+  rewrite Ring.IntID.mulrC exprM eq_inzmod_one expr1z.
+  rewrite mul1r exp_inzmod modz_ge0 /=; [by rewrite gtr_eqF|].
+  by rewrite modz_abs.
+qed.
+
+lemma exp_mod (x : zmod) n k :
+  exp x k = one =>
+  exp x n = exp x (n %% k).
+proof.
+  case: (k = 0) => [->>|neqk0]; [by rewrite modz0|].
+  rewrite -(asintK x) => eq_exp_one; rewrite exp_inzmod.
+  case: (0 <= n) => [le0n|Nle0n].
+  + rewrite (inzmod_exp_mod (asint x) n k).
+    - move: eq_exp_one; rewrite exp_inzmod.
+      by case (0 <= k) => // _; rewrite exprN invr_eq1.
+    by rewrite le0n /= inzmod_exp modz_ge0.
+  rewrite -(invrK (exp (inzmod _) _)); apply congr1.
+  rewrite -exprN -(mul1r (ZModField.ZModpField.exp _ _)).
+  rewrite -(expr1z (- n %/ k)) -eq_exp_one -exprM mulrN Ring.IntID.mulrC -exprD.
+  + apply/negP => eq_inzmod_zero; move: eq_inzmod_zero eq_exp_one => ->.
+    by rewrite expr0z neqk0 /= eq_sym oner_neq0.
+  by rewrite -opprD -divz_eq inzmod_exp oppr_ge0 ltzW //= ltrNge.
+qed.
+
+(*FIXME*)
+lemma exp_sub_p_1 (x : zmod) :
+  unit x =>
+  exp x (p - 1) = one.
+proof.
+admitted.
+
+lemma exp_p (x : zmod) :
+  exp x p = x.
+proof.
+  case: (unit x) => [unitx|].
+  + by rewrite -(Ring.IntID.subrK p 1) exprD -?unitE // expr1 exp_sub_p_1 // mul1r.
+  rewrite unitE /= => ->; rewrite expr0z.
+  by move: prime_p; rewrite /prime; case (p = 0) => // ->.
+qed.
+
+lemma inv_exp_sub_p_2 x :
+  unit x =>
+  inv x = exp x (p - 2).
+proof.
+  move => unitx; rewrite -div1r; move: (eqf_div one x (exp x (p - 2)) one).
+  rewrite -unitE unitx oner_neq0 -div1r !mul1r divr1 /= -exprSr /=.
+  + by rewrite subr_ge0 ge2_p.
+  by rewrite exp_sub_p_1.
+qed.
+
 end ZModField.
diff --git a/theories/analysis/RealExp.ec b/theories/analysis/RealExp.ec
index 6902233676..c1a3b096f2 100644
--- a/theories/analysis/RealExp.ec
+++ b/theories/analysis/RealExp.ec
@@ -3,6 +3,7 @@ require import AllCore StdRing StdOrder RealFun.
 require import FinType.
 (*---*) import IntOrder RField RealOrder.
 require import List.
+require import IntDiv.
 
 (* -------------------------------------------------------------------- *)
 op exp : real -> real.
@@ -234,6 +235,10 @@ move=> gt1_b gt0_x gt0_y @/log; rewrite ler_pmul2r.
 - by apply/ln_mono.
 qed.
 
+(*-----------------------------------------------------------------------------*)
+lemma logM (a x y : real) : 0%r < x => 0%r < y => log a (x * y) = log a x + log a y.
+proof. by move => lt0x lt0y; rewrite -mulrDl -lnM. qed.
+
 (* -------------------------------------------------------------------- *)
 lemma rpowK (b x : real) : 0%r < b => b <> 1%r => 0%r < x =>
   b ^ (log b x) = x.
@@ -299,7 +304,8 @@ have := log_ge0 b%r x%r _ _; rewrite ?le_fromint //.
 by move/ler_lt_trans => /(_ _ h); rewrite lt_fromint ltzS.
 qed.
 
-lemma ilogP (b x : int) : 1 < b => 1 <= x =>
+lemma ilogP (b x : int) :
+  1 < b => 1 <= x =>
   b ^ ilog b x <= x < b ^ (ilog b x + 1).
 proof.
 rewrite -!(lt_fromint, le_fromint) => gt1_b ge1_x;
@@ -316,6 +322,67 @@ rewrite -!(lt_fromint, le_fromint) => gt1_b ge1_x;
   by rewrite fromintD -ltr_subl_addr &(floor_gt).
 qed.
 
+lemma ilog_eq (b x n : int) : 1 < b => 0 < x => 0 <= n => ilog b x = n <=> b ^ n <= x < b ^ (n + 1).
+proof.
+move => lt1b lt0x le0n; split => [<<-|]; first by apply ilogP; smt().
+move => [lepowx ltxpow]; apply/floorP; split => [|_].
++ rewrite -(logK b%r n%r) 1,2:/# log_mono 1,3:/#.
+  - by rewrite rpow_int 1:/# RealOrder.expr_gt0 /#.
+  by rewrite rpow_int 1:/# RField.fromintXn 1:/# le_fromint.
+rewrite -fromintD -(logK b%r (n + 1)%r) 1,2:/# RealOrder.ltrNge -negP log_mono 1,3:/#.
++ by rewrite rpow_int 1:/# RealOrder.expr_gt0 /#.
+by rewrite negP -RealOrder.ltrNge rpow_int 1:/# RField.fromintXn 1:/# lt_fromint.
+qed.
+
+lemma ilog_powK (b n : int) : 1 < b => 0 <= n => ilog b (b ^ n) = n.
+proof.
+move => lt1b le0n; rewrite /ilog -RField.fromintXn // -rpow_int 1: /#.
+by rewrite logK 1,2:/#; apply from_int_floor.
+qed.
+
+op is_pow b x = b ^ (ilog b x) = x.
+
+lemma is_powP (b x : int) : 1 < b => 0 < x => is_pow b x <=> exists n , 0 <= n /\ x = b ^ n.
+proof.
+move => lt1b lt0x; split.
++ by move => His_pow; exists (ilog b x); rewrite His_pow /= ilog_ge0 /#.
+by move => [n [le0n ->]]; rewrite /is_pow ilog_powK.
+qed.
+
+lemma ilog_mull (b x y : int) : 1 < b => 0 < x => 0 < y => is_pow b x => ilog b (x * y) = ilog b x + ilog b y.
+proof.
+move => lt1b lt0x lt0y /(is_powP _ _ lt1b lt0x) [n [le0n ->>]].
+rewrite /ilog -RField.fromintXn // -rpow_int 1:/# fromintM logM //.
++ by rewrite lt_fromint; apply IntOrder.expr_gt0; move: (IntOrder.ltr_naddr 1 (-1) b _ lt1b) => // ->.
++ by rewrite lt_fromint.
+rewrite -RField.fromintXn // -rpow_int 1:/# logK ?le_fromint // 1,2:/#.
+by rewrite from_int_floor from_int_floor_addl.
+qed.
+
+lemma ilog_mulr (b x y : int) : 1 < b => 0 < x => 0 < y => is_pow b y => ilog b (x * y) = ilog b x + ilog b y.
+proof. by move => lt1b lt0x lt0y; rewrite mulrC addrC; apply ilog_mull. qed.
+
+lemma ilog_b b : 1 < b => ilog b b = 1.
+proof. by move => lt1b; rewrite -(ilog_powK b 1) // expr1. qed.
+
+lemma ilog_mono b x y : 1 < b => 0 < x => x <= y => ilog b x <= ilog b y.
+proof. by move => lt1b lt0x lt0y; apply/floor_mono/log_mono; rewrite ?le_fromint ?lt_fromint //; apply (IntOrder.ltr_le_trans x). qed.
+
+lemma ilog_small b x : 1 < b => 0 < x < b => ilog b x = 0.
+proof.
+move => lt1b [lt0x ltxb]; rewrite floorP -fromintD /=; split => [|_]; first by apply/log_ge0 => /#.
+by rewrite -(logK b%r 1%r) 1,2:/# rpow_int 1:/# expr1 RealOrder.ltrNge log_mono; smt().
+qed.
+
+lemma ilog_dvd (b x : int) : 0 < x => 1 < b => b <= x => ilog b x = ilog b (x %/ b) + 1.
+proof.
+move => lt0x lt1b lebx; apply ilog_eq => //; first by smt(ilog_ge0).
+have []:= (ilogP b (x %/ b) _ _) => //; first by rewrite lez_divRL //= /#.
+by rewrite lez_divRL 1:/# ltz_divLR 1:/# -!exprSr //; smt(ilog_ge0).
+qed.
+
+hint simplify ilog_small, ilog_dvd.
+
 (* -------------------------------------------------------------------- *)
 require import StdBigop.
 (*---*) import Bigreal BRA BRM.
diff --git a/theories/datatypes/BitEncoding.ec b/theories/datatypes/BitEncoding.ec
index 64a6c50be3..31f6370b06 100644
--- a/theories/datatypes/BitEncoding.ec
+++ b/theories/datatypes/BitEncoding.ec
@@ -20,6 +20,24 @@ proof. by apply/size_mkseq. qed.
 lemma bs2int_nil : bs2int [] = 0.
 proof. by rewrite /bs2int BIA.big_geq. qed.
 
+lemma bs2int_cons x s :
+  bs2int (x :: s) = b2i x + 2 * bs2int s.
+proof.
+  rewrite /bs2int /= (addrC 1) Bigint.BIA.big_int_recl ?size_ge0 /= expr0 /=.
+  congr => //; rewrite Bigint.BIA.mulr_sumr; apply Bigint.BIA.eq_big_seq.
+  move => K /= HK_range; rewrite (@eqz_leq _ 0) -ltzE ltzNge.
+  move/mem_range: (HK_range) => [-> _] /=.
+  by rewrite mulrA exprS //; move/mem_range: HK_range.
+qed.
+
+lemma bs2int_nseq_false N :
+  bs2int (nseq N false) = 0.
+proof.
+  case (0 <= N) => [le0N|/ltzNge/ltzW leN0]; last by rewrite nseq0_le // bs2int_nil.
+  elim N le0N => /=; rewrite ?nseq0 ?bs2int_nil // => N le0N.
+  by rewrite nseqS // bs2int_cons /b2i => ->.
+qed.
+
 lemma nosmt bs2int_rcons b (s : bool list):
   bs2int (rcons s b) = (bs2int s) + 2^(size s) * (b2i b).
 proof.
@@ -42,10 +60,63 @@ move/ltrNge => @/max ^gt0_N ->/= i lt_in.
 by rewrite nth_nseq ?nth_mkseq //= div0z mod0z.
 qed.
 
+lemma int2bs_nseq_false N n :
+  (2 ^ N) %| n =>
+  int2bs N n = nseq N false.
+proof.
+  move => /dvdzP [q ->>]; rewrite /int2bs -mkseq_nseq.
+  apply eq_in_mkseq => K /mem_range HK_range /=.
+  apply negeqF => /=; rewrite -IntDiv.divzpMr.
+  + by apply dvdz_exp2l; move/mem_range: HK_range => [-> /ltzW].
+  rewrite -IntDiv.exprD_subz //; first by move/mem_range: HK_range => [-> /ltzW].
+  rewrite -dvdzE dvdz_mull; move: (dvdz_exp2l 2 1 (N - K)); rewrite expr1 /= => -> //.
+  by apply/ltzS/ltr_subl_addr/ltr_subr_addr; move/mem_range: HK_range.
+qed.
+
 lemma nosmt int2bsS N i : 0 <= N =>
   int2bs (N + 1) i = rcons (int2bs N i) ((i %/ 2^N) %% 2 <> 0).
 proof. by apply/mkseqS. qed.
 
+lemma int2bs_cons N n :
+  0 < N =>
+  int2bs N n = (!2 %| n) :: int2bs (N - 1) (n %/ 2).
+proof.
+  move => lt0N; rewrite /int2bs; move: (subrK N 1) => {1}<-; rewrite mkseqSr /=; first by apply/subr_ge0; move/ltzE: lt0N.
+  rewrite expr0 dvdzE /=; apply eq_in_mkseq => K [le0K _]; rewrite /(\o) /=.
+  by rewrite -divz_mul // -exprS // (addrC 1).
+qed.
+
+lemma int2bs_rcons N n :
+  0 < N =>
+  int2bs N n = rcons (int2bs (N - 1) n) ((n %/ 2 ^ (N - 1)) %% 2 <> 0).
+proof. by move => lt0N; rewrite -int2bsS // subr_ge0; move: lt0N; rewrite ltzE. qed.
+
+lemma int2bs_mod N n :
+  int2bs N (n %% 2 ^ N) = int2bs N n.
+proof.
+  apply eq_in_mkseq => K /mem_range HK_range /=.
+  rewrite IntDiv.modz_pow2_div; first by move/mem_range: HK_range => [-> /=]; apply ltzW.
+  rewrite modz_dvd //; move: (dvdz_exp2l 2 1 (N - K)); rewrite expr1 => /= -> //.
+  by apply/ler_subr_addl/ltzE; move/mem_range: HK_range.
+qed.
+
+lemma int2bs_nseq_true N :
+  int2bs N (2 ^ N - 1) = nseq N true.
+proof.
+  rewrite /int2bs -mkseq_nseq.
+  apply eq_in_mkseq => K /mem_range HK_range /=.
+  rewrite divzDl.
+  + by apply dvdz_exp2l; move/mem_range: HK_range => [-> /ltzW].
+  rewrite -IntDiv.exprD_subz //; first by move/mem_range: HK_range => [-> /ltzW].
+  rewrite dvdz_modzDl.
+  + move: (dvdz_exp2l 2 1 (N - K)); rewrite expr1 /= => -> //.
+    by rewrite ler_subr_addr addrC -ltzE; case/mem_range: HK_range.
+  move: (subrK (-1) (2 ^ K)) => <-; rewrite addrAC (addrC (-1)).
+  rewrite divzDr; [by rewrite -{2}(mul1r (2 ^ K)) -mulNr dvdz_mull dvdzz|].
+  rewrite divz_small; [by rewrite normrX ltzE //= subr_ge0 -ltzS ltr_addr expr_gt0|].
+  by rewrite -{1}(mul1r (2 ^ K)) -mulNr mulzK //=; apply/gtr_eqF/expr_gt0.
+qed.
+
 lemma nosmt bs2int_eq N i j: 0 <= i => 0 <= j => i %% 2^N = j %% 2^N =>
   int2bs N i = int2bs N j.
 proof.
@@ -58,12 +129,6 @@ move/(congr1 (fun z => z %% 2^1))=> /=; rewrite !modz_dvd_pow /=;
 by rewrite !expr1 => ->.
 qed.
 
-lemma nosmt bs2int_mod N i : 0 <= i => int2bs N (i %% 2^N) = int2bs N i.
-proof.
-move=> ge0_i; apply/bs2int_eq=> //; last by rewrite modz_mod.
-by rewrite modz_ge0 // -lt0n ?ltrW // expr_gt0.
-qed.
-
 lemma bs2int_ge0 s : 0 <= bs2int s.
 proof.
 elim/last_ind: s => /= [|s b ih]; 1: by rewrite bs2int_nil.
@@ -83,8 +148,8 @@ lemma bs2intK s : int2bs (size s) (bs2int s) = s.
 proof.
 elim/last_ind: s=> /= [|s b ih]; 1: by rewrite bs2int_nil int2bs0s.
 rewrite bs2int_rcons size_rcons int2bsS ?size_ge0.
-rewrite -(@bs2int_mod (size s)) 1:-bs2int_rcons ?bs2int_ge0.
-rewrite mulrC modzMDr bs2int_mod 1:bs2int_ge0 ih; congr.
+rewrite -(@int2bs_mod (size s)).
+rewrite mulrC modzMDr int2bs_mod; congr.
 have gt0_2Xs: 0 < 2  ^ (size s) by rewrite expr_gt0.
 rewrite divzMDr 1:gtr_eqF // divz_small /=.
   by rewrite bs2int_ge0 gtr0_norm ?bs2int_le2Xs.
@@ -98,16 +163,392 @@ move=> ge0N; elim: N ge0N i=> /= [|n ge0_n ih] i.
   rewrite expr0 ltz1 -eqr_le => <-; rewrite int2bs0.
   by rewrite nseq0_le // bs2int_nil.
 case=> [ge0_i lt_i2XSn]; rewrite int2bsS // bs2int_rcons.
-rewrite -{1}bs2int_mod // ih 1:ltz_pmod ?expr_gt0 //=.
-  by rewrite modz_ge0 gtr_eqF ?expr_gt0.
+rewrite -{1}int2bs_mod // ih //=.
+  by rewrite modz_ge0 ?gtr_eqF ?ltz_pmod ?expr_gt0.
 rewrite size_int2bs ler_maxr // eq_sym {1}(@divz_eq i (2^n)).
 rewrite addrC mulrC; do 2! congr; move: lt_i2XSn.
 rewrite exprS // -ltz_divLR ?expr_gt0 // => lt.
 rewrite -{1}(@modz_small (i %/ 2^n) 2) ?ger0_norm ?b2i_mod2 //.
 by rewrite lt /= divz_ge0 ?expr_gt0.
 qed.
+
+(* -------------------------------------------------------------------- *)
+lemma int2bs_cat K N n :
+  0 <= K <= N =>
+  int2bs N n = (int2bs K n) ++ (int2bs (N - K) (n %/ (2 ^ K))).
+proof.
+  move => [le0K leKN]; rewrite /int2bs.
+  rewrite -{1}(@subrK N K) (@addrC _ K).
+  rewrite mkseq_add ?subr_ge0 //.
+  congr; apply eq_in_mkseq => I /= [le0I _].
+  by rewrite exprD_nneg // IntDiv.divz_mul // expr_ge0.
+qed.
+
+lemma int2bs1 N :
+  0 < N =>
+  int2bs N 1 = true :: nseq (N - 1) false.
+proof. by move => lt0N; rewrite int2bs_cons // dvdzE /= int2bs_nseq_false. qed.
+
+lemma int2bs_cat_nseq_true_false K N :
+  0 <= K <= N =>
+  int2bs N (2 ^ K - 1) = nseq K true ++ nseq (N - K) false.
+proof.
+  move => le2; move: (int2bs_cat _ _ (2 ^ K - 1) le2) => ->.
+  rewrite int2bs_nseq_true divz_small; [by rewrite normrX ltzE //= subr_ge0 -ltzS ltr_addr expr_gt0|].
+  by rewrite int2bs0.
+qed.
+
+lemma int2bs_mulr_pow2 K N n :
+  0 <= K <= N =>
+  int2bs N (2 ^ K * n) = nseq K false ++ int2bs (N - K) n.
+proof.
+  move => [le0K leKN]; rewrite /int2bs.
+  rewrite -{1}(@subrK N K) (@addrC _ K).
+  move: (subrK N K) => {1}<-.
+  move: (addrC (N - K) K) => ->.
+  rewrite mkseq_add //; first by apply/subr_ge0/ler_subl_addl => /=; apply/subr_ge0.
+  rewrite -/int2bs.
+  rewrite -(@int2bs_nseq_false _ (2 ^ K * n)).
+  + by apply/dvdz_mulr/dvdzz.
+  congr; rewrite // (addrC K) -(addrA N) /=.
+  apply eq_in_mkseq => I /= /mem_range HI_range.
+  rewrite exprD_nneg //; first by move/mem_range: HI_range.
+  by rewrite divzMpl //; apply expr_gt0.
+qed.
+
+lemma int2bs_divr_pow2 K N n :
+  int2bs N (n %/ 2 ^ K) = drop `|K| (int2bs (N + `|K|) n).
+proof.
+  rewrite pow_normr; case (0 <= N) => [le0N|/ltzNge/ltzW leN0]; last first.
+  + by rewrite drop_oversize; [rewrite size_int2bs ler_maxrP normr_ge0 ler_naddl|rewrite int2bs0s_le].
+  rewrite (@int2bs_cat `|K| (N + `|K|)) ?normr_ge0 ?lez_addr //= drop_size_cat -?addrA //=.
+  by rewrite size_int2bs ler_maxr // normr_ge0.
+qed.
+
+lemma int2bs_pow2 K N :
+  K \in range 0 N =>
+  int2bs N (2 ^ K) = nseq K false ++ true :: nseq (N - 1 - K) false.
+proof.
+  move => HK_range; move: (int2bs_mulr_pow2 K N 1) => /= ->.
+  + by split; move/mem_range: HK_range => // [_ ltKN] _; apply ltzW.
+  rewrite int2bs1; first by apply subr_gt0; move/mem_range:HK_range.
+  by rewrite addrAC.
+qed.
+
+(*-----------------------------------------------------------------------------*)
+lemma bs2int_cat s1 s2 :
+  bs2int (s1 ++ s2) = bs2int s1 + (2 ^ (size s1)) * bs2int s2.
+proof.
+  elim/last_ind: s2 => [|s2 b]; first by rewrite cats0 bs2int_nil.
+  rewrite -rcons_cat !bs2int_rcons mulrDr addrA mulrA size_cat => ->.
+  by rewrite exprD_nneg ?size_ge0.
+qed.
+
+lemma bs2int_range s :
+  bs2int s \in range 0 (2 ^ size s).
+proof. by apply/mem_range; split; [apply bs2int_ge0|move => _; apply bs2int_le2Xs]. qed.
+
+lemma bs2int1 N :
+  bs2int (true :: nseq N false) = 1.
+proof. by rewrite bs2int_cons bs2int_nseq_false /b2i. qed.
+
+lemma bs2int_nseq_true N :
+  0 <= N =>
+  bs2int (nseq N true) = 2 ^ N - 1.
+proof.
+  move => le0N; rewrite -int2bs_nseq_true int2bsK //.
+  by rewrite ltzE //= subr_ge0 -ltzS ltr_addr expr_gt0.
+qed.
+
+lemma bs2int_cat_nseq_true_false K N :
+  0 <= K <= N =>
+  bs2int (nseq K true ++ nseq (N - K) false) = 2 ^ K - 1.
+proof.
+  move => le2; rewrite -int2bs_cat_nseq_true_false // int2bsK //.
+  + by move: le2 => [? ?]; apply/(ler_trans K).
+  by rewrite ltzE //= subr_ge0 -ltzS ltr_addr expr_gt0 //= ler_weexpn2l.
+qed.
+
+lemma bs2int_mulr_pow2 N s :
+  bs2int (nseq N false ++ s) = 2 ^ max 0 N * bs2int s.
+proof. by rewrite bs2int_cat bs2int_nseq_false size_nseq. qed.
+
+lemma bs2int_pow2 K N :
+  bs2int (nseq K false ++ true :: nseq N false) = 2 ^ max 0 K.
+proof. by rewrite bs2int_mulr_pow2 bs2int1. qed.
+
 end BS2Int.
 
+
+(* -------------------------------------------------------------------- *)
+theory BitReverse.
+
+import BS2Int.
+
+op bsrev N n = bs2int (rev (int2bs N n)).
+
+lemma int2bs_bsrev N n :
+  int2bs N (bsrev N n) = rev (int2bs N n).
+proof.
+  rewrite /bsrev; move: (bs2intK (rev (int2bs N n))).
+  rewrite size_rev size_int2bs /max.
+  by case (0 < N) => // /lezNgt ?; rewrite !int2bs0s_le.
+qed.
+
+lemma bsrev_bs2int s :
+  bsrev (size s) (bs2int s) = bs2int (rev s).
+proof. by rewrite /bsrev bs2intK. qed.
+
+lemma bsrev_neg N n :
+  N <= 0 =>
+  bsrev N n = 0.
+proof. by rewrite /bsrev => leN0; move: (size_int2bs N n); rewrite ler_maxl // size_eq0 => ->; rewrite rev_nil bs2int_nil. qed.
+
+lemma bsrev_cons N n :
+  0 < N =>
+  bsrev N n = 2 ^ (N - 1) * b2i (!2 %| n) + bsrev (N - 1) (n %/ 2).
+proof.
+  move => lt0N; rewrite /bsrev int2bs_cons // rev_cons -cats1 bs2int_cat size_rev size_int2bs ler_maxr; first by rewrite -ltzS.
+  by rewrite bs2int_cons; move: (bs2int_nseq_false 0); rewrite nseq0 => -> /=; rewrite addrC.
+qed.
+
+lemma bsrev_ge0 N n :
+  0 <= bsrev N n.
+proof. by rewrite /bsrev bs2int_ge0. qed.
+
+lemma bsrev_lt_pow2 N n :
+  bsrev N n < 2 ^ N.
+proof.
+  case (0 <= N) => [le0N|/ltrNge /ltzW leN0]; last by rewrite bsrev_neg // expr_gt0.
+  rewrite /bsrev; move: (bs2int_le2Xs (rev (int2bs N n))).
+  by rewrite size_rev size_int2bs ler_maxr.
+qed.
+
+lemma bsrev_range N n :
+  bsrev N n \in range 0 (2 ^ N).
+proof. by rewrite mem_range bsrev_ge0 bsrev_lt_pow2. qed.
+
+lemma bsrev_cat K N n :
+  0 <= K <= N =>
+  bsrev N n = bsrev (N - K) (n %/ 2 ^ K) + 2 ^ (N - K) * bsrev K n.
+proof. by move => [le0K leKN]; rewrite /bsrev (@int2bs_cat K) // rev_cat bs2int_cat size_rev size_int2bs ler_maxr // subr_ge0. qed.
+
+lemma bsrev_mod N n :
+  bsrev N (n %% 2 ^ N) = bsrev N n.
+proof. by rewrite /bsrev int2bs_mod. qed.
+
+lemma bsrev_involutive N n :
+  0 <= N =>
+  n \in range 0 (2 ^ N) =>
+  bsrev N (bsrev N n) = n.
+proof.
+  move => le0N Hn_range; rewrite /bsrev.
+  move: (bs2intK (rev (int2bs N n))).
+  rewrite size_rev size_int2bs ler_maxr // => ->.
+  by rewrite revK int2bsK // -mem_range.
+qed.
+
+lemma bsrev_injective N n1 n2 :
+  0 <= N =>
+  n1 \in range 0 (2 ^ N) =>
+  n2 \in range 0 (2 ^ N) =>
+  bsrev N n1 = bsrev N n2 =>
+  n1 = n2.
+proof. by move => le0N Hn1_range Hn2_range eq_bsrev; rewrite -(@bsrev_involutive N n1) // -(@bsrev_involutive N n2) // eq_bsrev. qed.
+
+lemma bsrev_bijective N n1 n2 :
+  0 <= N =>
+  n1 \in range 0 (2 ^ N) =>
+  n2 \in range 0 (2 ^ N) =>
+  bsrev N n1 = bsrev N n2 <=>
+  n1 = n2.
+proof. by move => le0n Hn1_range Hn2_range; split => [|-> //]; apply bsrev_injective. qed.
+
+lemma bsrev0 N :
+  bsrev N 0 = 0.
+proof. by rewrite /bsrev int2bs0 rev_nseq bs2int_nseq_false. qed.
+
+lemma bsrev1 N :
+  0 < N =>
+  bsrev N 1 = 2 ^ (N - 1).
+proof.
+  move => lt0N; rewrite /bsrev int2bs1 // rev_cons bs2int_rcons rev_nseq.
+  by rewrite size_nseq bs2int_nseq_false /b2i /= ler_maxr // subr_ge0; move/ltzE: lt0N.
+qed.
+
+lemma bsrev_mulr_pow2 K N n :
+  0 <= K <= N =>
+  bsrev N (2 ^ K * n) = bsrev N n %/ 2 ^ K.
+proof.
+  move => [le0K leKN]; rewrite /bsrev int2bs_mulr_pow2 // rev_cat rev_nseq bs2int_cat bs2int_nseq_false /=.
+  rewrite (@int2bs_cat (N - K) N); first by split; [rewrite subr_ge0|move => _; rewrite ler_subl_addr ler_addl].
+  rewrite rev_cat bs2int_cat size_rev size_int2bs opprD addrA /= ler_maxr // (mulrC (exp _ _)%IntDiv) divzMDr.
+  + by apply/gtr_eqF/expr_gt0.
+  by rewrite divz_small // -mem_range normrX_nat // bsrev_range.
+qed.
+
+lemma bsrev_divr_pow2 K N n :
+  0 <= K <= N =>
+  bsrev N (n %/ 2 ^ K) = (bsrev (N + K) n) %% (2 ^ N).
+proof.
+  move => [le0K leKN]; rewrite /bsrev int2bs_divr_pow2 ger0_norm // /int2bs drop_mkseq.
+  + by split => // _; rewrite ler_addr (lez_trans K).
+  rewrite -addrA /= addrC mkseq_add //; first by apply/(lez_trans K).
+  rewrite rev_cat bs2int_cat size_rev size_mkseq ler_maxr //; first by apply/(lez_trans K).
+  rewrite mulrC modzMDr modz_small //.
+  rewrite -mem_range normrX_nat; first by apply/(lez_trans K).
+  move: (bs2int_range (rev (mkseq (fun (i : int) => (fun (i0 : int) => n %/ 2 ^ i0 %% 2 <> 0) (K + i)) N))).
+  by rewrite size_rev size_mkseq ler_maxr //; apply/(lez_trans K).
+qed.
+
+lemma bsrev_pow2 K N :
+  K \in range 0 N =>
+  bsrev N (2 ^ K) = 2 ^ (N - 1 - K).
+proof.
+  move => HK_range; move: (bsrev_mulr_pow2 K N 1) => /= ->; first by rewrite (@ltzW K); move/mem_range: HK_range.
+  rewrite bsrev1; first by apply/(ler_lt_trans K); move/mem_range: HK_range.
+  by rewrite -exprD_subz //= -(@ltzS K); move/mem_range: HK_range.
+qed.
+
+lemma bsrev_range_dvdz K N n :
+  0 <= K <= N =>
+  n \in range 0 (2 ^ (N - K)) =>
+  2 ^ K %| bsrev N n.
+proof.
+  move => [le0K leKN] Hn_range; rewrite (@bsrev_cat (N - K)) //.
+  + by rewrite subr_ge0 leKN /= ler_subl_addl -ler_subl_addr.
+  rewrite opprD addrA /= divz_small; first by rewrite -mem_range normrX_nat // subr_ge0.
+  by rewrite bsrev0 /= dvdz_mulr dvdzz.
+qed.
+
+lemma bsrev_dvdz_range K N n :
+  0 <= K <= N =>
+  (2 ^ (N - K)) %| n =>
+  bsrev N n \in range 0 (2 ^ K).
+proof.
+  move => [le0K leKN] dvdz_n; rewrite (@bsrev_cat (N - K)).
+  + by rewrite subr_ge0 leKN /= ler_subl_addl -ler_subl_addr.
+  rewrite opprD addrA /=; move/dvdzP: dvdz_n => [q ->>].
+  rewrite (mulrC q) bsrev_mulr_pow2.
+  + by rewrite subr_ge0 leKN.
+  rewrite (@divz_small (bsrev _ _)) /=; last by apply bsrev_range.
+  by rewrite -mem_range normrX_nat ?subr_ge0 // bsrev_range.
+qed.
+
+lemma bsrev_add K N m n :
+  0 <= K <= N =>
+  m \in range 0 (2 ^ K) =>
+  bsrev N (m + 2 ^ K * n) = bsrev N m + bsrev N n %/ 2 ^ K.
+proof.
+  move => [le0K leKN] Hm_range; rewrite (@bsrev_cat K) //.
+  rewrite (mulrC (exp _ _)) divzMDr; first by apply/gtr_eqF/expr_gt0.
+  rewrite divz_small /=; first by rewrite -mem_range normrX_nat.
+  rewrite -(@bsrev_mod K) modzMDr bsrev_mod (addrC (bsrev _ _)); congr.
+  + rewrite (@bsrev_cat K N) // divz_small; last by rewrite bsrev0.
+    by rewrite -mem_range normrX_nat.
+  rewrite (@bsrev_cat (N - K) N).
+  + by split; [rewrite subr_ge0|move => _; rewrite ler_subl_addr ler_addl].
+  rewrite !opprD addrA /= (mulrC (exp _ _)) divzMDr.
+  + by apply/gtr_eqF/expr_gt0.
+  by rewrite divz_small // -mem_range normrX_nat // bsrev_range.
+qed.
+
+lemma bsrev2_le M N n :
+  0 <= M <= N =>
+  bsrev M (bsrev N n) = n %% 2 ^ N %/ 2 ^ (N - M).
+proof.
+  move => [le0M leMN]; rewrite -(@bsrev_mod N) /bsrev (@int2bs_cat (N - M) N).
+  + by rewrite subr_ge0 ler_subl_addl -ler_subl_addr.
+  rewrite opprD addrA /= rev_cat bs2int_cat size_rev size_int2bs ler_maxr //.
+  rewrite -{1}int2bs_mod mulrC modzMDr int2bs_mod.
+  move: (bsrev_involutive M (n %% 2 ^ N %/ 2 ^ (N - M)) _ _) => //.
+  rewrite range_div_range /=; first by apply/expr_gt0.
+  rewrite -exprD_nneg //; first by apply/subr_ge0.
+  rewrite addrA addrAC /=; move: (mem_range_mod n (2 ^ N)).
+  by rewrite normrX_nat; [apply/(lez_trans M)|move => -> //; apply/gtr_eqF/expr_gt0].
+qed.
+
+lemma bsrev2_ge M N n :
+  0 <= N <= M =>
+  bsrev M (bsrev N n) = 2 ^ (M - N) * (n %% 2 ^ N).
+proof.
+  move => [le0N leNM]; rewrite -(@bsrev_mod N) /bsrev (@int2bs_cat N M) //.
+  rewrite divz_small; first by rewrite -mem_range normrX_nat // bsrev_range.
+  rewrite int2bs0 rev_cat rev_nseq bs2int_cat size_nseq ler_maxr ?subr_ge0 //.
+  rewrite bs2int_nseq_false /=; congr; move: (bsrev_involutive N (n %% 2 ^ N) _ _) => //.
+  by move: (mem_range_mod n (2 ^ N)); rewrite normrX_nat; [apply/(lez_trans N)|move => -> //; apply/gtr_eqF/expr_gt0].
+qed.
+
+lemma bsrev_range_pow2_perm_eq K N :
+  0 <= K <= N =>
+  perm_eq
+    (map (bsrev N)             (range 0 (2 ^ K)))
+    (map (( * ) (2 ^ (N - K))) (range 0 (2 ^ K))).
+proof.
+  move => [le0K leKN]; rewrite perm_eqP_pred1 => x.
+  rewrite !count_uniq_mem.
+  + rewrite map_inj_in_uniq ?range_uniq // => {x} x y Hx_range Hy_range.
+    apply/bsrev_injective; first last.
+    - by move: Hx_range; apply/mem_range_incl => //; apply/ler_weexpn2l.
+    - by move: Hy_range; apply/mem_range_incl => //; apply/ler_weexpn2l.
+    by apply/(lez_trans K).
+  + rewrite map_inj_in_uniq ?range_uniq // => {x} x y Hx_range Hy_range.
+    by apply/mulfI/gtr_eqF/expr_gt0.
+  congr; rewrite eq_iff !mapP; split => -[y [Hy_range ->>]].
+  + exists (bsrev N y %/ (2 ^ (N - K))).
+    rewrite mulrC divzK /=.
+    - apply/bsrev_range_dvdz; last by rewrite opprD addrA.
+      by rewrite subr_ge0 leKN /= ger_addl oppz_le0.
+    rewrite range_div_range ?expr_gt0 //= -exprD_nneg ?subr_ge0 //.
+    by rewrite addrA addrAC /= bsrev_range.
+  exists (bsrev N y %/ (2 ^ (N - K))).
+  rewrite -bsrev_mulr_pow2 ?bsrev_involutive /=.
+  + by rewrite subr_ge0 leKN /= ger_addl oppz_le0.
+  + by apply/(lez_trans K).
+  + rewrite mem_range_mull ?expr_gt0 //=.
+    rewrite -(@mulN1r (exp _ _)%Int) -divzpMr.
+    - by rewrite dvdz_exp2l subr_ge0 leKN /= ger_addl oppz_le0.
+    rewrite mulN1r opprK -exprD_subz // ?opprD ?addrA //=.
+    by rewrite subr_ge0 leKN /= ger_addl oppz_le0.
+  by rewrite bsrev_dvdz_range // dvdz_mulr dvdzz.
+qed.
+
+lemma bsrev_mul_range_pow2_perm_eq K M N :
+  0 <= K =>
+  0 <= M =>
+  K + M <= N =>
+  perm_eq
+    (map (bsrev N \o (( * ) (2 ^ M))) (range 0 (2 ^ K)))
+    (map (( * ) (2 ^ (N - K - M)))    (range 0 (2 ^ K))).
+proof.
+  move => le0K le0M le_N.
+  move: (eq_in_map (bsrev N \o ( * ) (2 ^ M)) (transpose (%/) (2 ^ M) \o (bsrev N)) (range 0 (2 ^ K))).
+  move => [Heq_map _]; move: Heq_map => -> => [x Hx_range|]; last rewrite map_comp.
+  + by rewrite /(\o) bsrev_mulr_pow2; first rewrite le0M /= (lez_trans (K + M)) // ler_addr.
+  move: (eq_in_map (( * ) (2 ^ (N - K - M))) ((transpose (fun (m d : int) => m %/ d) (2 ^ M)) \o (( * ) (2 ^ (N - K)))) (range 0 (2 ^ K))).
+  move => [Heq_map _]; move: Heq_map => -> => [x Hx_range|].
+  + rewrite /(\o) /= -!(mulrC x) -divzpMr.
+    - by rewrite dvdz_exp2l le0M /= ler_subr_addl.
+    by rewrite -exprD_subz // le0M /= ler_subr_addl.
+  rewrite (@map_comp (transpose _ _) (( * )%Int _)) perm_eq_map bsrev_range_pow2_perm_eq.
+  by rewrite le0K /= (lez_trans (K + M)) // ler_addl.
+qed.
+
+lemma bsrev_cat_nseq_true_false K N :
+  0 <= K <= N =>
+  bsrev N (2 ^ K - 1) = 2 ^ N - 2 ^ (N - K).
+proof.
+  move => [? ?]; rewrite /bsrev int2bs_cat_nseq_true_false //.
+  rewrite rev_cat !rev_nseq bs2int_mulr_pow2 bs2int_nseq_true // ler_maxr.
+  + by rewrite subr_ge0.
+  rewrite mulrDr -exprD_nneg //=.
+  + by rewrite subr_ge0.
+  by rewrite -addrA /= mulrN.
+qed.
+
+end BitReverse.
+
+
 (* -------------------------------------------------------------------- *)
 theory BitChunking.
 op chunk r (bs : 'a list) =
diff --git a/theories/datatypes/Int.ec b/theories/datatypes/Int.ec
index 62b78e6b93..21a0e30f59 100644
--- a/theories/datatypes/Int.ec
+++ b/theories/datatypes/Int.ec
@@ -323,60 +323,6 @@ elim/intwlog: z1 => [z1 /#| |z1] /=; 1: by rewrite odd0.
 by move=> ge0_z1 ih; rewrite mulzDl /= oddS oddD ih /#.
 qed.
 
-(* -------------------------------------------------------------------- *)
-op argmin (f : int -> 'a) (p : 'a -> bool) =
-  choiceb (fun j => 0 <= j /\ p (f j) /\ forall i, 0 <= i < j => !p (f i)) 0.
-
-lemma argmin_out (f : int -> 'a) p: (forall i, !p (f i)) => argmin f p = 0.
-proof. by move=> pN; rewrite /argmin choiceb_dfl => //= x; rewrite pN. qed.
-
-lemma nosmt argminP_r (f : int -> 'a) p i: 0 <= i => p (f i) =>
-     0 <= argmin f p
-  /\ p (f (argmin f p))
-  /\ forall i, 0 <= i < (argmin f p) => !p (f i).
-proof.
-pose F := fun i0 => forall j, 0 <= j < i0 => !p (f j).
-move=> ge0_i pi; have: exists j, 0 <= j /\ p (f j) /\ F j.
-  elim/sintind: i ge0_i pi => i ge0_i ih pi.
-  case: (exists j, (0 <= j < i) /\ p (f j)).
-    by case=> j [/ih {ih} ih/ih]; apply.
-  move=> h; exists i; rewrite pi ge0_i => j lt_ji; apply/negP.
-  by move=> pj; apply/h; exists j; rewrite pj.
-by move/choicebP/(_ 0); apply.
-qed.
-
-lemma argminP (f : int -> 'a) p i: 0 <= i => p (f i) => p (f (argmin f p)).
-proof. by move=> ge0_i/(argminP_r _ _ _ ge0_i). qed.
-
-lemma ge0_argmin (f : int -> 'a) p: 0 <= argmin f p.
-proof.                          (* FIXME: choice_spec *)
-case: (exists i, 0 <= i /\ p (f i)); first by case=> i [] /(argminP_r f p) h /h.
-move=> h; rewrite /argmin choiceb_dfl ?lez_lt_asym //=.
-by move=> x; apply/negP=> [# ge0_x px xmin]; apply/h; exists x.
-qed.
-
-lemma argmin_min (f : int -> 'a) p: forall j, 0 <= j < argmin f p => !p (f j).
-proof.                          (* FIXME: choice_spec *)
-case: (exists i, 0 <= i /\ p (f i)); first by case=> i [] /(argminP_r f p) h /h.
-move=> h j; rewrite /argmin choiceb_dfl ?lez_lt_asym //=.
-by move=> x; apply/negP=> [# ge0_x px xmin]; apply/h; exists x.
-qed.
-
-lemma argmin_eq ['a] f p i :
-  0 <= i => p (f i) => (forall j, 0 <= j < i => !p (f j)) => argmin<:'a> f p = i.
-proof.
-move=> ge0_i pfi Npfj @/argmin.
-pose Q j := 0 <= j /\ p (f j) /\ forall i, 0 <= i < j => !p (f i).
-have /# := choicebP Q 0 _; first by exists i.
-qed.
-
-lemma argmin_le ['a] f p q :
-  (forall j, p j => q j) => argmin<:'a> f q <= argmin<:'a> f p.
-proof. move=> le_pq. admitted.
-
-(* -------------------------------------------------------------------- *)
-abbrev minz = argmin (fun (i : int) => i).
-
 (* -------------------------------------------------------------------- *)
 (* TO BE REMOVED                                                        *)
 
@@ -399,3 +345,19 @@ proof. elim/intind: n1; smt(fold0 foldS). qed.
 (* -------------------------------------------------------------------- *)
 op min (a b:int) = if (a < b) then a else b.
 op max (a b:int) = if (a < b) then b else a.
+
+lemma lez_minl a b :
+  a <= b => min a b = a.
+proof. by smt(). qed.
+
+lemma lez_minr a b :
+  b <= a => min a b = b.
+proof. by smt(). qed.
+
+lemma lez_maxl a b :
+  b <= a => max a b = a.
+proof. by smt(). qed.
+
+lemma lez_maxr a b :
+  a <= b => max a b = b.
+proof. by smt(). qed.
diff --git a/theories/datatypes/IntMin.ec b/theories/datatypes/IntMin.ec
index cb19b0578b..3fc174f713 100644
--- a/theories/datatypes/IntMin.ec
+++ b/theories/datatypes/IntMin.ec
@@ -3,6 +3,219 @@ require import AllCore Int.
 require (*--*) Ring StdOrder.
 (*---*) import Ring.IntID StdOrder.IntOrder.
 
+(* -------------------------------------------------------------------- *)
+op argmin (f : int -> 'a) (p : 'a -> bool) =
+  choiceb (fun j => 0 <= j /\ p (f j) /\ forall i, 0 <= i < j => !p (f i)) 0.
+
+lemma argmin_out (f : int -> 'a) p: (forall i, 0 <= i => !p (f i)) => argmin f p = 0.
+proof.
+move=> pN; rewrite /argmin choiceb_dfl => //= x; rewrite !negb_and -implybE => le0x.
+by rewrite -implybE => px; move: (pN _ le0x).
+qed.
+
+lemma nosmt argminP_r (f : int -> 'a) p i: 0 <= i => p (f i) =>
+     0 <= argmin f p
+  /\ p (f (argmin f p))
+  /\ forall i, 0 <= i < (argmin f p) => !p (f i).
+proof.
+pose F := fun i0 => forall j, 0 <= j < i0 => !p (f j).
+move=> ge0_i pi; have: exists j, 0 <= j /\ p (f j) /\ F j.
+  elim/sintind: i ge0_i pi => i ge0_i ih pi.
+  case: (exists j, (0 <= j < i) /\ p (f j)).
+    by case=> j [/ih {ih} ih/ih]; apply.
+  move=> h; exists i; rewrite pi ge0_i => j lt_ji; apply/negP.
+  by move=> pj; apply/h; exists j; rewrite pj.
+by move/choicebP/(_ 0); apply.
+qed.
+
+lemma argminP (f : int -> 'a) p i: 0 <= i => p (f i) => p (f (argmin f p)).
+proof. by move=> ge0_i/(argminP_r _ _ _ ge0_i). qed.
+
+lemma ge0_argmin (f : int -> 'a) p: 0 <= argmin f p.
+proof.                          (* FIXME: choice_spec *)
+case: (exists i, 0 <= i /\ p (f i)); first by case=> i [] /(argminP_r f p) h /h.
+move=> h; rewrite /argmin choiceb_dfl ?lez_lt_asym //=.
+by move=> x; apply/negP=> [# ge0_x px xmin]; apply/h; exists x.
+qed.
+
+lemma argmin_min (f : int -> 'a) p: forall j, 0 <= j < argmin f p => !p (f j).
+proof.                          (* FIXME: choice_spec *)
+case: (exists i, 0 <= i /\ p (f i)); first by case=> i [] /(argminP_r f p) h /h.
+move=> h j; rewrite /argmin choiceb_dfl ?lez_lt_asym //=.
+by move=> x; apply/negP=> [# ge0_x px xmin]; apply/h; exists x.
+qed.
+
+lemma argmin_eq ['a] f p i :
+  0 <= i => p (f i) => (forall j, 0 <= j < i => !p (f j)) => argmin<:'a> f p = i.
+proof.
+move=> ge0_i pfi Npfj @/argmin.
+pose Q j := 0 <= j /\ p (f j) /\ forall i, 0 <= i < j => !p (f i).
+have /# := choicebP Q 0 _; first by exists i.
+qed.
+
+lemma le_argmin ['a] f p i :
+  0 <= i =>
+  ((exists j, (0 <= j) /\ (p (f j))) => (exists j, (0 <= j <= i) /\ (p (f j)))) <=>
+  (argmin<:'a> f p <= i).
+proof.
+move => le0i; case (exists j, (0 <= j) /\ (p (f j))) => /= [[j [le0j pj]]|].
++ split => [|le_i]; last by exists (argmin f p); rewrite le_i ge0_argmin /=; apply/(argminP _ _ j).
+  move => [k [[le0k leki] pk]]; apply/lezNgt/negP => lti_; apply/(argmin_min f p k) => //.
+  by split => // _; apply/(ler_lt_trans i).
+by move => /negb_exists /= Npj; rewrite argmin_out // => j; move: (Npj j); rewrite negb_and -implybE.
+qed.
+
+lemma ge_argmin ['a] f p i :
+  0 < i =>
+  ((exists j, (0 <= j) /\ (p (f j))) /\ (forall j, (0 <= j < i) => !(p (f j)))) <=>
+  (i <= argmin<:'a> f p).
+proof.
+move => lt0i; case (exists j, (0 <= j) /\ (p (f j))) => /= [[j [le0j pj]]|].
++ split => [|lei_ k [le0k ltki]]; last by apply argmin_min; rewrite le0k /=; apply (ltr_le_trans i).
+  move => Npk; apply/lezNgt/negP => lt_i; apply (Npk (argmin f p)); first by rewrite lt_i ge0_argmin.
+  by apply (argminP _ _ j).
+move => /negb_exists /= Npj; apply/ltrNge; rewrite argmin_out // => j.
+by move: (Npj j); rewrite negb_and -implybE.
+qed.
+
+lemma argmin_le ['a] f p q :
+  (exists j, (0 <= j) /\ (p (f j))) =>
+  (forall j, 0 <= j => p (f j) => q (f j)) =>
+  argmin<:'a> f q <= argmin<:'a> f p.
+proof.
+move=> pj le_pq; apply/le_argmin; first by apply/ge0_argmin.
+move=> [j [le0j qj]]; exists (argmin f p); rewrite ge0_argmin /=.
+by apply le_pq; [rewrite ge0_argmin|move: pj => [k [le0k pk]]; apply (argminP _ _ k)].
+qed.
+
+(* -------------------------------------------------------------------- *)
+abbrev minz = argmin (fun (i : int) => i).
+
+(* -------------------------------------------------------------------- *)
+op argmax ['a] (f : int -> 'a) (p : 'a -> bool) : int =
+  choiceb (fun (j : int) => 0 <= j /\ p (f j) /\ forall (i : int), j < i => ! p (f i)) 0.
+
+lemma argmax_out (f : int -> 'a) p:
+(forall i, 0 <= i => !p (f i)) \/
+(forall i, 0 <= i => exists j, i <= j /\ p (f j)) =>
+argmax f p = 0.
+proof.
+move=> [pN|pij]; rewrite /argmax choiceb_dfl => //= x; rewrite !negb_and -implybE => le0x; rewrite -implybE => px; first by move: (pN _ le0x).
+by rewrite negb_forall /=; move: (pij (x + 1) _); [rewrite addz_ge0|move => [j [lejx pj]]; exists j; rewrite negb_imply ltzE].
+qed.
+
+lemma argmaxP_r (f : int -> 'a) p i j:
+  0 <= i =>
+  0 <= j =>
+  p (f i) =>
+  (forall k, j <= k => !(p (f k))) =>
+     0 <= argmax f p
+  /\ p (f (argmax f p))
+  /\ forall i, (argmax f p) < i => !p (f i).
+proof.
+pose F := fun i0 => forall (j : int), i0 < j => !p (f j).
+move=> ge0_i ge0_j pi pnj; have: exists k, 0 <= k /\ p (f k) /\ F k.
+  elim/sintind: j ge0_j pnj => j ge0_j ih pnj.
+  case: (exists k, (0 <= k < j) /\ (forall (l : int), k <= l => ! p (f l))); first by case=> k [/ih].
+  move=> h; exists (j-1); apply/and_impr; split => [|le0_]; [|split].
+    by move/ler_eqVlt: ge0_j => [<<-|]; [move: (pnj i); rewrite ge0_i pi|move/ltzE/ler_subr_addr].
+    by apply/negbNE/negP => pn_; apply/h; exists (j-1); rewrite le0_ ltzE //= => l /ler_eqVlt [<<- //|/ltzE /= /pnj].
+  by move => k /ltzE /=; apply pnj.
+by move/choicebP/(_ 0); apply.
+qed.
+
+lemma argmaxP (f : int -> 'a) p i j:
+  0 <= i =>
+  0 <= j =>
+  p (f i) =>
+  (forall k, j <= k => !(p (f k))) =>
+  p (f (argmax f p)).
+proof. by move => ge0i ge0j Hpfi Hnpfj; move: (argmaxP_r _ _ _ _ _ _ Hpfi Hnpfj). qed.
+
+lemma ge0_argmax (f : int -> 'a) p:
+  0 <= argmax f p.
+proof.                          (* FIXME: choice_spec *)
+case: (exists i j, 0 <= i /\ 0 <= j /\ p (f i) /\ (forall k, j <= k => !(p (f k)))).
++ by case=> i j [? [? [Hpfi Hnpfj]]]; move: (argmaxP_r _ _ _ _ _ _ Hpfi Hnpfj).
+move=> h; rewrite /argmax choiceb_dfl ?lez_lt_asym //=.
+move=> x; apply/negP=> [# ge0_x px xmax]; apply/h; exists x; exists (x + 1).
+by do!split => //; [apply addz_ge0|move => k; rewrite -ltzE; apply xmax].
+qed.
+
+lemma argmax_max (f : int -> 'a) p j:
+  0 <= j =>
+  (forall k, j <= k => !(p (f k))) =>
+  forall j, argmax f p < j => !p (f j).
+proof.                          (* FIXME: choice_spec *)
+case: (exists i, 0 <= i /\ p (f i)).
++ by case=> i [? Hpfi] ? Hnpfj; move: (argmaxP_r _ _ _ _ _ _ Hpfi Hnpfj).
+move=> h i; rewrite /argmax choiceb_dfl ?lez_lt_asym //=.
++ by move=> x; apply/negP=> [# le0x Hpfx Hnpfx]; apply/h; exists x.
+by move => _ k lt0k; apply/negP => Hpfk; apply/h; exists k; split => //; apply/ltzW.
+qed.
+
+lemma argmax_eq ['a] f p i :
+  0 <= i => p (f i) => (forall j, i < j => !p (f j)) => argmax<:'a> f p = i.
+proof.
+move=> ge0_i pfi Npfj @/argmax.
+pose Q j := 0 <= j /\ p (f j) /\ forall i, j < i => !p (f i).
+by have /# := choicebP Q 0 _; exists i.
+qed.
+
+lemma le_argmax ['a] f p i :
+  0 <= i =>
+  ((exists j, (0 <= j) /\ (forall k, (j <= k) => !(p (f k)))) => (forall j, i < j => !(p (f j)))) <=>
+  (argmax<:'a> f p <= i).
+proof.
+move => le0i; case ((forall i, 0 <= i => !p (f i)) \/ (forall i, 0 <= i => exists j, i <= j /\ p (f j))) => /=.
++ move => Hor; rewrite argmax_out // le0i /=; case Hor => [Npj _ j ltij|]; first by apply/Npj/(lez_trans i) => //; apply ltzW.
+  by move => pj [j [le0j Npk]]; case (pj _ le0j) => k [lejk pkj]; move: (Npk _ lejk).
+move => /negb_or [/negb_forall [j /= /negb_imply [le0j /= pj]] /negb_forall [k /= /negb_imply [le0k /negb_exists /= Npl]]].
+have ->/=: (exists (l : int), 0 <= l /\ forall (m : int), l <= m => ! p (f m)).
++ by exists k; split => // l ltkl; move: (Npl l) => /negb_and; rewrite ltkl.
+split => [Npi|le_i l leil].
++ apply/lezNgt/negP => /(Npi _); apply/negP => /=; apply/(argmaxP _ _ _ (i + 1) le0j _ pj _); first by apply addz_ge0.
+  by move => l /ltzE; apply Npi.
+apply (argmax_max _ _ _ le0k _ _ _); last by apply (ler_lt_trans i) => //.
+by move => m lekm; move: (Npl m) => /negb_and; rewrite lekm.
+qed.
+
+lemma ge_argmax ['a] f p i :
+  0 < i =>
+  ((exists j, (0 <= j) /\ (forall k, (j <= k) => !(p (f k)))) /\ (exists j, (i <= j) /\ (p (f j)))) <=>
+  (i <= argmax<:'a> f p).
+proof.
+move => lt0i; case ((forall i, 0 <= i => !p (f i)) \/ (forall i, 0 <= i => exists j, i <= j /\ p (f j))) => /=.
++ move => Hor; rewrite argmax_out // (lezNgt i) lt0i /=; apply/negb_and; case Hor => [Npj|pj].
+  - by right; apply/negb_exists => /= j; apply/negb_and/implybE => leij; apply/Npj/(lez_trans i) => //; apply/ltzW.
+  left; apply/negb_exists => /= j; apply/negb_and/implybE => le0j; apply/negb_forall; move: (pj _ le0j).
+  by move => /= [k [lejk pk]]; exists k; apply/negb_imply; split.
+move => /negb_or [/negb_forall [j /= /negb_imply [le0j /= pj]] /negb_forall [k /= /negb_imply [le0k /negb_exists /= Npl]]].
+have ->/=: (exists (l : int), 0 <= l /\ forall (m : int), l <= m => ! p (f m)).
++ by exists k; split => // l ltkl; move: (Npl l) => /negb_and; rewrite ltkl.
+split => [[l [leil pl]]|lei_]; last by exists (argmax f p); split => //; apply/(argmaxP _ _ _ k le0j le0k pj _) => l lekl; move: (Npl l); rewrite lekl.
+apply/lezNgt/negP => lt_i.
+(*FIXME: why no one liner? Pierre-Yves*)
+have lt_l:= (ltr_le_trans _ _ _ lt_i leil).
+by move: (argmax_max _ _ _ le0k _ _ lt_l); [move => m lekm; move: (Npl m); rewrite lekm|].
+qed.
+
+lemma argmax_le ['a] f p q :
+  (exists j, (0 <= j) /\ (forall k, (j <= k) => !(q (f k)))) =>
+  (forall j, 0 <= j => p (f j) => q (f j)) =>
+  argmax<:'a> f p <= argmax<:'a> f q.
+proof.
+move => [i [le0i Nqk]] le_pq; apply le_argmax; first by apply ge0_argmax.
+move => [j [le0j Npk]] k /ltzE /ler_subr_addr le__; move: (le__); rewrite -le_argmax.
++ by apply/(lez_trans (argmax f q)) => //; apply/ge0_argmax.
+move => HNq; apply/negP => pk; apply (HNq _ k); [by exists i|by apply/ltzE| ].
+apply le_pq => //; apply (lez_trans (argmax f q)); first apply ge0_argmax.
+by apply (lez_trans (k-1)) => //; apply/ltzW/ltzE.
+qed.
+
+(* -------------------------------------------------------------------- *)
+abbrev maxz = argmax (fun (i : int) => i).
+
 (* -------------------------------------------------------------------- *)
 op pcap (E : int -> bool) =
   fun x => 0 <= x /\ E x.
@@ -60,6 +273,18 @@ rewrite eqr_le pmin_min //= lerNgt; apply/negP=> gti.
 by apply/(min_i (pmin E))/pmin_mem => //; rewrite ge0_pmin.
 qed.
 
+lemma pmin_nmem E i : ! sempty (pcap E) => 0 <= i < pmin E => ! E i.
+proof.
+move => Hnsempty [le0i ltipmin]; apply/negP => HEi.
+by move: (ltr_le_trans _ _ _ ltipmin (pmin_min _ _ Hnsempty le0i HEi)).
+qed.
+
+lemma pmin_max E i : ! sempty (pcap E) => 0 <= i => (forall j , 0 <= j < i => ! E j) => i <= pmin E.
+proof.
+move=> h ge0_i min_i; rewrite lerNgt; apply/negP=> gti.
+by apply/(min_i (pmin E))/pmin_mem => //; rewrite ge0_pmin.
+qed.
+
 (* -------------------------------------------------------------------- *)
 op fmin_spec ['a] (f : 'a -> int) (p : 'a -> bool) (x : 'a) =
   0 <= f x /\ p x /\ forall y, 0 <= f y => p y => f x <= f y.
diff --git a/theories/datatypes/List.ec b/theories/datatypes/List.ec
index 9fe0e8e028..7b61be2dad 100644
--- a/theories/datatypes/List.ec
+++ b/theories/datatypes/List.ec
@@ -432,6 +432,12 @@ proof. by elim: s=> //= x s; smt. qed.
 lemma count_size p (s : 'a list): count p s <= size s.
 proof. by elim: s => //= x s; smt. qed.
 
+lemma mem_count ['a] x (s : 'a list) : (x \in s) <=> (0 < count (pred1 x) s).
+proof.
+  elim: s => //= hs ts IHs; rewrite /b2i {1}/pred1 (eq_sym x).
+  by case (hs = x) => /= _ //; rewrite addrC ltzS count_ge0.
+qed.
+
 op has (p : 'a -> bool) xs =
   with xs = []      => false
   with xs = y :: ys => (p y) \/ (has p ys).
@@ -535,6 +541,9 @@ proof. by rewrite all_count count_predT. qed.
 lemma all_predC p (s : 'a list): all (predC p) s = ! has p s.
 proof. by elim: s => //= x s ->; rewrite /predC; case: (p x). qed.
 
+lemma all_predI p1 p2 (s : 'a list): all (predI p1 p2) s = (all p1 s /\ all p2 s).
+proof. by elim: s => //= x s ->; rewrite /predI /=; case: (p1 x); case (p2 x). qed.
+
 lemma eq_filter_in p1 p2 (s : 'a list):
   (forall x, x \in s => p1 x <=> p2 x) => filter p1 s = filter p2 s.
 proof.
@@ -932,7 +941,18 @@ qed.
 op rotr n (s : 'a list) = rot (size s - n) s.
 
 lemma rotK n: cancel<:'a list, 'a list> (rot n) (rotr n).
-proof. smt. qed.
+proof.
+move => s.
+case (lez_total 0 n) => [le0n|len0]; last first.
+  by rewrite rot_le0 // /rotr rot_oversize //; smt.
+case (lez_total n (size s)) => [lens|lesn]; last first.
+  by rewrite rot_oversize // /rotr rot_le0 //; smt.
+rewrite -{2}(cat_take_drop n s) /rotr {1}/rot; congr.
+  by rewrite size_rot drop_size_cat // size_drop //; smt.
+by rewrite size_rot take_size_cat // size_drop //; smt.
+(*FIXME: not working somehow.*)
+(*smt.*)
+qed.
 
 lemma rot_inj n (s1 s2 : 'a list): rot n s1 = rot n s2 => s1 = s2.
 proof. by apply (can_inj (rot n) (rotr n)); apply rotK. qed.
@@ -1159,6 +1179,24 @@ elim: s => //= z s ih; rewrite (@fun_if (rem x)) (@fun_if (rem y)) /= ih.
 by case: (z = x); case: (z = y).
 qed.
 
+lemma perm_eqP_pred1 ['a] (s1 s2 : 'a list) : perm_eq s1 s2 <=> forall (x : 'a), count (pred1 x) s1 = count (pred1 x) s2.
+proof.
+  rewrite perm_eqP; split => [Heq x|Heq p]; first by apply/Heq.
+  elim s1 s2 Heq => [s2 /= Heq|hs1 ts1 IHs1 s2 /= Heq].
+  + elim: s2 Heq => //= hs2 ts2 IHs2 Heq.
+    move: (Heq hs2); rewrite /b2i /pred1 /= eqz_leq => -[_].
+    by rewrite addrC -ltzE ltzNge count_ge0.
+  move: IHs1 => /(_ (rem hs1 s2)) => ->.
+  + move => x; move: (Heq hs1) (Heq x) => {Heq}.
+    rewrite {1}/b2i {1}/pred1 /= => Heqhs1.
+    rewrite (count_rem (pred1 x) s2 hs1); last by apply addrI.
+    by rewrite mem_count -Heqhs1 addrC ltzS count_ge0.
+  move: (Heq hs1) => {Heq}.
+  rewrite {1}/b2i {1}/pred1 /= => Heqhs1.
+  rewrite (count_rem p s2 hs1) //.
+  by rewrite mem_count -Heqhs1 addrC ltzS count_ge0.
+qed.
+
 (* -------------------------------------------------------------------- *)
 (*                        Element insertion                             *)
 (* -------------------------------------------------------------------- *)
@@ -1313,6 +1351,28 @@ qed.
 lemma perm_eq_rev (s : 'a list) : perm_eq s (rev s).
 proof. by rewrite perm_eqP=> p; rewrite count_rev. qed.
 
+lemma rev_drop ['a] n (s : 'a list) :
+  0 <= n <= size s =>
+  rev (drop n s) = take (size s - n) (rev s).
+proof.
+move => [le0n lensizes]; rewrite -(cat_take_drop n s) drop_size_cat.
+  by rewrite size_take //; move: lensizes => [->|->>].
+rewrite rev_cat size_cat size_take // size_drop //.
+rewrite lez_maxr ?subz_ge0 // !addzA /=.
+have ->: ((if n < size s then n else size s) = n) by move: lensizes => [->|->>].
+rewrite (addrC n) -(addrA (size _)) /= take_size_cat //.
+by rewrite size_rev size_drop // lez_maxr // subz_ge0.
+qed.
+
+lemma rev_take ['a] n (s : 'a list) :
+  0 <= n <= size s =>
+  rev (take n s) = drop (size s - n) (rev s).
+proof.
+move => [? ?]; apply rev_inj; rewrite revK rev_drop.
+  by rewrite size_rev; smt().
+by rewrite revK size_rev opprD opprK addrA.
+qed.
+
 (* -------------------------------------------------------------------- *)
 (*                        Duplicate-freenes                             *)
 (* -------------------------------------------------------------------- *)
@@ -1652,6 +1712,16 @@ proof.
   by rewrite mem_behead.
 qed.
 
+lemma map_uniq_inj_in ['b, 'a] (f : 'a -> 'b) (s : 'a list) :
+     uniq (map f s)
+  => forall x y, mem s x => mem s y => f x = f y => x = y.
+proof.
+  elim: s => // z s ih /= [Nmemfx uniqfs] x y [<<-|memxs] [<<-|memys] eqf //.
+    by move: Nmemfx; rewrite eqf map_f.
+    by move: Nmemfx; rewrite -eqf map_f.
+  by apply ih.
+qed.
+
 lemma mem_map_fst (xs : ('a * 'b) list) (x : 'a):
   mem (map fst xs) x <=> (exists y, mem xs (x,y)).
 proof.
@@ -2070,6 +2140,78 @@ theory Range.
   lemma nth_range  (i p k w : int):
     0 <= i < p - k => nth w (range k p) i = k + i.
   proof. by apply/nth_iota. qed.
+
+  lemma le2_mem_range (m n i: int):
+    (m <= i <= n) <=> (mem (range m (n+1)) i).
+  proof. by rewrite mem_range ltzS. qed.
+
+  lemma mem_range_le (m n i j: int):
+    j <= m =>
+    mem (range m n) i =>
+    j <= i.
+  proof. by move => lejm /mem_range [lemi _]; apply/(lez_trans m). qed.
+
+  lemma mem_range_gt (m n i j: int):
+    n <= j =>
+    mem (range m n) i =>
+    i < j.
+  proof. by move => lenj /mem_range [_ ltin]; rewrite ltzE (lez_trans n) // -ltzE. qed.
+
+  lemma mem_range_lt (m n i j: int):
+    j < m =>
+    mem (range m n) i =>
+    j < i.
+  proof. by rewrite !ltzE; apply mem_range_le. qed.
+
+  lemma mem_range_ge (m n i j: int):
+    n <= j + 1 =>
+    mem (range m n) i =>
+    i <= j.
+  proof. by move => ?; rewrite -ltzS; apply mem_range_gt. qed.
+
+  lemma mem_range_incl (m1 n1 m2 n2 i : int) :
+    m2 <= m1 =>
+    n1 <= n2 =>
+    i \in range m1 n1 =>
+    i \in range m2 n2.
+  proof. by rewrite !mem_range => ? ? [? ?]; split;smt(). qed.
+
+  lemma mem_range_addl (m n x y : int) :
+    x + y \in range m n <=> y \in range (m - x) (n - x).
+  proof. by rewrite !mem_range; smt(). qed.
+
+  lemma mem_range_addr (m n x y : int) :
+    x + y \in range m n <=> x \in range (m - y) (n - y).
+  proof. by rewrite addrC mem_range_addl. qed.
+
+  lemma mem_range_add2 (m1 n1 m2 n2 x y : int) :
+    x \in range m1 n1 =>
+    y \in range m2 n2 =>
+    x + y \in range (m1 + m2) (n1 + n2 - 1).
+  proof. by rewrite !mem_range => -[? ?] [? ?]; smt(). qed.
+
+  lemma mem_range_opp (m n x : int) :
+    -x \in range m n <=> x \in range (- n + 1) (- m + 1).
+  proof. by rewrite !mem_range -ltzE ltzS; smt(). qed.
+
+  lemma mem_range_subl (m n x y : int) :
+    x - y \in range m n <=> y \in range (- n + x + 1) (- m + x + 1).
+  proof. by rewrite mem_range_addl mem_range_opp !opprD. qed.
+
+  lemma mem_range_subr (m n x y : int) :
+    x - y \in range m n <=> x \in range (m + y) (n + y).
+  proof. by rewrite mem_range_addr. qed.
+
+  lemma mem_range_mul (m1 n1 m2 n2 x y : int) :
+    0 <= m1 =>
+    0 <= m2 =>
+    x \in range m1 n1 =>
+    y \in range m2 n2 =>
+    x * y \in range (m1 * m2) (n1 * n2 - n1 - n2 + 2).
+  proof.
+    by rewrite !mem_range => le0m1 le0m2 [lem1x ltxn1] [lem2x ltn2]; split;  smt().
+  qed.
+
 end Range.
 
 export Range.
@@ -2220,6 +2362,9 @@ lemma mkseqS f n : 0 <= n =>
   mkseq<:'a> f (n + 1) = rcons (mkseq f n) (f n).
 proof. by move=> ge0_n; rewrite /mkseq iotaSr //= map_rcons. qed.
 
+lemma mkseqSr ['a] (f : int -> 'a) n : 0 <= n => mkseq f (n + 1) = f 0 :: mkseq (f \o ((+)%Int 1)) n.
+proof. by move => le0n; rewrite /mkseq iotaS //= map_comp -iota_addl. qed.
+
 lemma mkseq_add (f : int -> 'a) n m : 0 <= n => 0 <= m =>
   mkseq f (n+m) = mkseq f n ++ mkseq (fun i => f (n+i)) m.
 proof.
@@ -2231,6 +2376,30 @@ lemma mkseqP f n (x:'a) :
   mem (mkseq f n) x <=> exists i, 0 <= i < n /\ x = f i.
 proof. by rewrite mapP &(exists_iff) /= => i; rewrite mem_iota. qed.
 
+lemma mkseq_nseq ['a] n (x : 'a) :
+  mkseq (fun _ => x) n = nseq n x.
+proof.
+  case (0 <= n) => [le0n|/ltzNge/ltzW len0]; last by rewrite mkseq0_le // nseq0_le.
+  elim n le0n => [|n le0n]; first by rewrite mkseq0 nseq0.
+  by rewrite nseqSr // mkseqS // => ->.
+qed.
+
+lemma drop_mkseq ['a] (f : int -> 'a) k n :
+  0 <= k <= n =>
+  drop k (mkseq f n) = mkseq (f \o ((+) k)) (n - k).
+proof.
+  move => [le0k lekn]; move: (mkseq_add f k (n - k) _ _) => //; first by smt().
+  by rewrite addrA addrAC /= => ->; rewrite drop_size_cat // size_mkseq lez_maxr.
+qed.
+
+lemma take_mkseq ['a] (f : int -> 'a) k n :
+  0 <= k <= n =>
+  take k (mkseq f n) = mkseq f k.
+proof.
+  move => [le0k lekn]; move: (mkseq_add f k (n - k) _ _) => //; first by smt().
+  by rewrite addrA addrAC /= => ->; rewrite take_size_cat // size_mkseq lez_maxr.
+qed.
+
 (* -------------------------------------------------------------------- *)
 (*                         Sequence folding                             *)
 (* -------------------------------------------------------------------- *)
@@ -2242,6 +2411,10 @@ lemma foldr_cat (f : 'a -> 'b -> 'b) z0 s1 s2:
   foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.
 proof. by elim: s1 => //= x s1 ->. qed.
 
+lemma foldr_rcons (f : 'a -> 'b -> 'b) z0 s z :
+  foldr f z0 (rcons s z) = foldr f (f z z0) s.
+proof. by rewrite -cats1 foldr_cat. qed.
+
 lemma foldr_map ['a 'b 'c] (f : 'a -> 'b -> 'b) (h : 'c -> 'a) z0 s:
   foldr f z0 (map h s) = foldr (fun x z, f (h x) z) z0 s.
 proof. by elim: s => //= x s ->. qed.
@@ -2263,6 +2436,14 @@ proof.
   by rewrite -(revK (s1 ++ s2)) foldl_rev rev_cat foldr_cat -!foldl_rev !revK.
 qed.
 
+lemma foldl_rcons (f : 'b -> 'a -> 'b) z0 s z :
+  foldl f z0 (rcons s z) = f (foldl f z0 s) z.
+proof. by rewrite -cats1 foldl_cat. qed.
+
+lemma foldl_map ['a 'b 'c] (f : 'b -> 'a -> 'b) (h : 'c -> 'a) z0 s:
+  foldl f z0 (map h s) = foldl (fun z x, f z (h x)) z0 s.
+proof. by elim: s z0 => //= x s ih z0; rewrite ih. qed.
+
 lemma foldr_perm (f : 'a -> 'b -> 'b) (z : 'b) (s1 s2 : 'a list):
      (forall a b v, f a (f b v) = f b (f a v))
   => perm_eq s1 s2
@@ -2284,6 +2465,23 @@ lemma foldr_rem (x : 'a) (f : 'a -> 'b -> 'b) (z : 'b) (s : 'a list):
   => foldr f z s = f x (foldr f z (rem x s)).
 proof. by move=> fAC /perm_to_rem peq; rewrite (@foldr_perm f z _ _ fAC peq). qed.
 
+lemma foldr_comp ['a, 'b, 'c] (f1 : 'b -> 'a -> 'a) (f2 : 'c -> 'b) z s : foldr (f1 \o f2) z s = foldr f1 z (map f2 s).
+proof. by elim s => //= hs ts ->; rewrite /(\o). qed.
+
+lemma eq_foldr ['a, 'b] (f1 f2 : 'a -> 'b -> 'b) z1 z2 s1 s2 :
+  (forall x , f1 x = f2 x) =>
+  z1 = z2 =>
+  s1 = s2 =>
+  foldr f1 z1 s1 = foldr f2 z2 s2.
+proof. by move => Heq <<- <<-; elim s1 => //= hs1 ts1 ->; rewrite Heq. qed.
+
+lemma eq_foldl ['a, 'b] (f1 f2 : 'a -> 'b -> 'a) z1 z2 s1 s2 :
+  (forall x y , f1 x y = f2 x y) =>
+  z1 = z2 =>
+  s1 = s2 =>
+  foldl f1 z1 s1 = foldl f2 z2 s2.
+proof. by move => Heq <<- <<-; elim s1 z1 => //= hs1 ts1 ih z1; rewrite ih Heq. qed.
+
 (* -------------------------------------------------------------------- *)
 (*                               EqIn                                   *)
 (* -------------------------------------------------------------------- *)
@@ -2325,6 +2523,65 @@ lemma eq_in_mkseq (f1 f2 : int -> 'a) n:
   => mkseq f1 n = mkseq f2 n.
 proof. by move=> h; rewrite -eq_in_map=> x /mema_iota /h. qed.
 
+lemma eq_in_foldr ['a, 'b] (f1 f2 : 'a -> 'b -> 'b) z1 z2 s1 s2 :
+  (forall x,  x \in s1 => f1 x = f2 x) =>
+  z1 = z2 =>
+  s1 = s2 =>
+  foldr f1 z1 s1 = foldr f2 z2 s2.
+proof. by move => Heq <<- <<-; elim s1 Heq => //= hs1 ts1 IHs1 Heq; rewrite IHs1 => [x Hin|]; rewrite Heq // Hin. qed.
+
+lemma eq_in_foldl ['a, 'b] (f1 f2 : 'a -> 'b -> 'a) z1 z2 s1 s2 :
+  (forall x y,  y \in s1 => f1 x y = f2 x y) =>
+  z1 = z2 =>
+  s1 = s2 =>
+  foldl f1 z1 s1 = foldl f2 z2 s2.
+proof. by move => Heq <<- <<-; elim s1 z1 Heq => //= hs1 ts1 IHs1 z1 Heq; rewrite IHs1 => [x y Hin|]; rewrite Heq // Hin. qed.
+
+op left_commutative_in ['b 'a] o (z : 'b) (s : 'a list) =
+  forall x y ,
+    x \in s =>
+    y \in s =>
+    o x (o y z) = o y (o x z).
+
+lemma foldr_perm_in ['b 'a] o (s1 s2 : 'a list) :
+  (forall (z : 'b) , left_commutative_in o z s1) =>
+  perm_eq s1 s2 =>
+  (forall (z : 'b) , foldr o z s1 = foldr o z s2).
+proof.
+  elim: s1 s2 => [|h1 t1 IHs1] s2 Hlci Heqs12 /=.
+  + by have -> //: s2 = []; apply/perm_eq_small/perm_eq_sym.
+  have/perm_eq_mem/(_ h1) := Heqs12; rewrite mem_head /=.
+  move/splitPr => [h2 t2] ->> z; rewrite foldr_cat /=.
+  move: Heqs12; rewrite -(cat1s h1 t2) catA perm_eq_sym.
+  rewrite perm_catCA /= perm_cons perm_eq_sym => Heqs1_.
+  move: (IHs1 _ _ Heqs1_); first by move => w a b Has1 Hbs1; apply/Hlci => /=; right.
+  move => ->; rewrite foldr_cat; have Heqin:= (perm_eq_mem _ _ Heqs1_).
+  have {Heqs1_ Heqin Hlci} Hlci: forall z , left_commutative_in o z (h1 :: h2).
+  + by move => w a b /= [->>|Hat1] [->>|Hbt2]; apply/Hlci => //=; right; rewrite Heqin mem_cat; left.
+  elim: h2 Hlci => [|x h2 {IHs1} IHs1 Hlci] //=.
+  rewrite -IHs1; first by move => w a b /= [->>|Has1] [->>|Hbs1] //; apply/Hlci => //=; rewrite ?Has1 ?Hbs1.
+  by rewrite Hlci.
+qed.
+
+op right_commutative_in ['a 'b] o (x : 'a) (s : 'b list) =
+  forall y z ,
+    y \in s =>
+    z \in s =>
+    o (o x y) z = o (o x z) y.
+
+lemma foldl_perm_in ['a 'b] o (s1 s2 : 'a list) :
+  (forall (x : 'b) , right_commutative_in o x s1) =>
+  perm_eq s1 s2 =>
+  (forall (x : 'b) , foldl o x s1 = foldl o x s2).
+proof.
+  move => rcomm peq x; rewrite -(revK s1) -(revK s2) !foldl_rev.
+  apply foldr_perm_in.
+  + move => {x} z x y; rewrite !mem_rev => mems1 mems2.
+    by rewrite rcomm.
+  apply/(perm_eq_trans s1); [by apply/perm_eq_sym/perm_eq_rev|].
+  by apply/(perm_eq_trans s2) => //; apply/perm_eq_rev.
+qed.
+
 (* -------------------------------------------------------------------- *)
 (*                            Flattening                                *)
 (* -------------------------------------------------------------------- *)
@@ -2820,6 +3077,20 @@ rewrite (map_zip_nth witness witness) //= &(eq_in_map).
 by move=> x /mem_range [? ?] /=; congr; rewrite index_uniq.
 qed.
 
+lemma foldr_zip_nseq ['a,'b,'c] (f : 'a -> 'b -> 'c -> 'c) x z s :
+  foldr (f x) z s = foldr (fun p => f (fst p) (snd p)) z (zip (nseq (size s) x) s).
+proof.
+  elim s => [|hs ts IHs] /=; first by rewrite nseq0.
+  by rewrite addrC nseqS ?size_ge0 //= IHs.
+qed.
+
+lemma foldl_zip_nseq ['a,'b,'c] (f : 'a -> 'c -> 'b -> 'c) x z s :
+  foldl (f x) z s = foldl (fun y p => f (fst p) y (snd p)) z (zip (nseq (size s) x) s).
+proof.
+  elim s z => [|hs ts IHs z] /=; first by rewrite nseq0.
+  by rewrite addrC nseqS ?size_ge0 //= IHs.
+qed.
+
 (* -------------------------------------------------------------------- *)
 (*                            All pairs                                 *)
 (* -------------------------------------------------------------------- *)
@@ -2836,6 +3107,14 @@ lemma allpairs_consl f x s t :
  allpairs<:'a, 'b, 'c> f (x :: s) t = map (f x) t ++ allpairs f s t.
 proof. by []. qed.
 
+lemma allpairs_consr f x s t :
+ perm_eq (allpairs<:'a, 'b, 'c> f s (x :: t)) (map (transpose f x) s ++ allpairs f s t).
+proof.
+  elim: s => [|h s ih]; [by rewrite allpairs0l|].
+  rewrite !allpairs_consl /= perm_cons catA perm_eq_sym.
+  by rewrite perm_catCA -catA perm_cat2l perm_eq_sym.
+qed.
+
 lemma size_allpairs ['a 'b 'c] f s t :
   size (allpairs<:'a, 'b, 'c> f s t) = size s * size t.
 proof.
@@ -2887,6 +3166,19 @@ move/perm_eq_trans; apply; elim: s3 => [|y s3 {ih} ih] /=.
 by rewrite catA perm_catCA -catA; apply/perm_cat2l/ih.
 qed.
 
+lemma allpairs_swap ['a 'b 'c] (f : 'a -> 'b -> 'c) s1 s2 :
+  perm_eq
+    (allpairs f s1 s2)
+    (allpairs (transpose f) s2 s1).
+proof.
+  elim: s1 => [|h1 t1 ih /=]; [by rewrite allpairs0l allpairs0r|].
+  rewrite allpairs_consl perm_eq_sym.
+  apply/(perm_eq_trans (map (transpose (transpose f) h1) s2 ++ allpairs (transpose f) s2 t1)).
+  + by apply/allpairs_consr.
+  rewrite (eq_map _ (f h1)); [by move => ?|].
+  by rewrite perm_cat2l perm_eq_sym.
+qed.
+
 (* -------------------------------------------------------------------- *)
 (*                         Sequence sorting                             *)
 (* -------------------------------------------------------------------- *)
diff --git a/theories/datatypes/Real.ec b/theories/datatypes/Real.ec
index 7fc21f4e0c..f23c021530 100644
--- a/theories/datatypes/Real.ec
+++ b/theories/datatypes/Real.ec
@@ -110,6 +110,9 @@ abbrev ( ^ ) = RField.exp.
 (* -------------------------------------------------------------------- *)
 lemma divr0: forall x, x / 0%r = 0%r by done.
 
+lemma divrK (u v : real) : v <> 0%r => u = u / v * v.
+proof. by move => neqv0; rewrite -mulrA mulVf. qed.
+
 lemma invr0: inv 0%r = 0%r by done.
 
 (* -------------------------------------------------------------------- *)
@@ -217,7 +220,7 @@ op floor : real -> int.
 op ceil  : real -> int.
 
 axiom floor_bound (x:real) : x - 1%r < (floor x)%r <= x.
-axiom  ceil_bound (x:real) : x <= (ceil x)%r < x + 1%r.
+axiom ceil_bound  (x:real) : x <= (ceil x)%r < x + 1%r.
 axiom from_int_floor n : floor n%r = n.
 axiom from_int_ceil  n : ceil  n%r = n.
 
@@ -233,6 +236,18 @@ proof. by case: (ceil_bound x). qed.
 lemma ceil_lt x : (ceil x)%r < x + 1%r.
 proof. by case: (ceil_bound x). qed.
 
+lemma floorP x n : floor x = n <=> n%r <= x < n%r + 1%r.
+proof. smt(floor_bound). qed.
+
+lemma from_int_floor_addl n x : floor (n%r + x) = n + floor x.
+proof. smt(floor_bound). qed.
+
+lemma from_int_floor_addr n x : floor (x + n%r) = floor x + n.
+proof. smt(floor_bound). qed.
+
+lemma floor_mono (x y : real) : x <= y => floor x <= floor y.
+proof. smt(floor_bound). qed.
+
 (* -------------------------------------------------------------------- *)
 (* WARNING Lemmas used by tactics: *)
 lemma nosmt upto2_abs (x1 x2 x3 x4 x5:real):
diff --git a/theories/looping/IterProc.eca b/theories/looping/IterProc.eca
index 5bef3bab05..311f79fecc 100644
--- a/theories/looping/IterProc.eca
+++ b/theories/looping/IterProc.eca
@@ -235,3 +235,18 @@ call Hf;auto=> ??[#]-> HP HI Hl _ /=;split.
 + by rewrite HI HP // <@ Hl=>/head_behead /(_ witness) {1}<-.
 by move=>_ ??->/= x Hx;apply/HP/(mem_drop 1).
 qed.
+
+lemma iter_inv_HL (O<:Orcl) (P:t -> bool) (Inv: glob O -> bool):
+  hoare [ O.f :
+          P x /\ Inv (glob O) ==>
+          Inv (glob O) ] =>
+  hoare [ Iter(O).iter :
+          (forall x, mem l x => P x) /\ Inv (glob O) ==>
+          Inv (glob O) ].
+proof.
+move=> Hf;proc.
+while ((forall x, mem l x => P x) /\ Inv (glob O));auto.
+call Hf;auto => ? [[HP HI] Hl]; split.
++ by rewrite HI HP // <@ Hl=>/head_behead /(_ witness) {1}<-.
+by move=>_ ?->/= x Hx;apply/HP/(mem_drop 1).
+qed.
diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec
index 1f8207798e..9136534043 100644
--- a/theories/prelude/Logic.ec
+++ b/theories/prelude/Logic.ec
@@ -83,6 +83,8 @@ pred preim ['a 'b] (f : 'a -> 'b) p x = p (f x).
 abbrev [-printing] transpose ['a 'b 'c] (f : 'a -> 'b -> 'c) (y : 'b) =
   fun x => f x y.
 
+lemma transposeP ['a, 'b, 'c] (f : 'a -> 'b -> 'c) (x : 'a) (y : 'b) : f x y = transpose f y x by done.
+
 (* -------------------------------------------------------------------- *)
 op eta_ (f : 'a -> 'b) = fun x => f x
   axiomatized by etaE.
@@ -449,6 +451,9 @@ lemma nosmt orb_id2r a b c : (!b => a = c) => a \/ b <=> c \/ b by smt().
 lemma nosmt negb_and a b : !(a /\ b) <=> !a \/ !b by smt().
 lemma nosmt negb_or  a b : !(a \/ b) <=> !a /\ !b by smt().
 
+lemma nosmt andlP a b c : a => ((a /\ b) => c) => b => c by [].
+lemma nosmt andrP a b c : a => ((b /\ a) => c) => b => c by [].
+
 (* -------------------------------------------------------------------- *)
 lemma nosmt negb_exists (P : 'a -> bool) :
   !(exists a, P a) <=> forall a, !P a
@@ -516,6 +521,17 @@ lemma nosmt oraP  b1 b2 : b1 \/ b2 <=> b1 \/ (!b1 => b2) by smt().
 lemma nosmt andabP b1 b2 : b1 && b2 <=> b1 /\ b2 by [].
 lemma nosmt orabP  b1 b2 : b1 || b2 <=> b1 \/ b2 by smt().
 
+(* -------------------------------------------------------------------- *)
+(*FIXME: may be useless because of rewrite, or may not be.*)
+lemma nosmt andb_id2 a b c d : (a <=> b) => (c <=> d) => ((a /\ c) <=> (b /\ d)) by [].
+lemma nosmt or_andl a b : (a \/ b) <=> ((a /\ !b) \/ b) by [].
+lemma nosmt or_andr a b : (a \/ b) <=> (a \/ (!a /\ b)) by [].
+lemma nosmt and_impl a b : (a /\ b) <=> ((b => a) /\ b) by [].
+lemma nosmt and_impr a b : (a /\ b) <=> ( a /\ (a => b)) by [].
+
+lemma nosmt negb_eqbl a b : ! (a <=> b) <=> (!a <=> b) by [].
+lemma nosmt negb_eqbr a b : ! (a <=> b) <=> (a <=> !b) by [].
+
 (* -------------------------------------------------------------------- *)
 lemma nosmt forall_orl (P : bool) (Q : 'a -> bool) :
   (P \/ (forall (x : 'a), Q x)) <=> forall (x : 'a), (P \/ Q x).
diff --git a/theories/structure/Discrete.ec b/theories/structure/Discrete.ec
index f816bac166..6ce45c4dee 100644
--- a/theories/structure/Discrete.ec
+++ b/theories/structure/Discrete.ec
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-require import AllCore Ring StdRing StdOrder List Finite.
+require import AllCore Ring StdRing StdOrder List Finite IntMin.
 (*---*) import IntID IntOrder.
 
 (* -------------------------------------------------------------------- *)