diff --git a/ecc_classic/cyclic_code.v b/ecc_classic/cyclic_code.v
index 0d6f54f3..69716df8 100644
--- a/ecc_classic/cyclic_code.v
+++ b/ecc_classic/cyclic_code.v
@@ -122,10 +122,12 @@ Lemma rcs'_rcs (R : idomainType) n (x : 'rV[R]_n.+1) : rcs' x = rcs x.
 Proof.
 rewrite /rcs' /rcs; apply/rowP => i; rewrite !mxE.
 case: ifPn => [/eqP -> |i0].
-  congr (x _ _); apply val_inj => /=.
-  by rewrite PermDef.fun_of_permE ffunE /= inordK.
+  congr (x _ _).
+  rewrite /rcs_perm/= unlock/= ffunE eqxx.
+  apply/val_inj => /=.
+  by rewrite inordK.
 congr (x _ _); apply val_inj => /=.
-rewrite PermDef.fun_of_permE ffunE /= inordK.
+rewrite unlock ffunE /= inordK.
   by rewrite (negPf i0) inordK // (ltn_trans _ (ltn_ord i)) // prednK // lt0n.
 by rewrite (ltn_trans _ (ltn_ord i)) // prednK // lt0n.
 Qed.
@@ -138,7 +140,7 @@ rewrite coef_add_poly coefXM coefCM coef_add_poly coefXn 2!coef_opp_poly coefC.
 case: ifPn => [/eqP ->|i0]; last rewrite subr0.
   rewrite 2!add0r mulrN1 coef_rVpoly /=.
   case: insubP => //= j _ j0.
-  rewrite mxE PermDef.fun_of_permE ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _).
+  rewrite mxE unlock ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _).
   by apply val_inj => /=; rewrite inordK.
 case/boolP : (i == n.+1) => [/eqP ->|in0].
   rewrite mulr1 2!coef_rVpoly /=.
@@ -148,7 +150,7 @@ case/boolP : (i == n.+1) => [/eqP ->|in0].
 rewrite mulr0 2!coef_rVpoly; case: insubP => /= [j|].
   rewrite ltnS => in0' ji; case: insubP => /= [k _ ki|].
     apply/eqP; rewrite subr_eq0; apply/eqP.
-    rewrite mxE PermDef.fun_of_permE ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _).
+    rewrite mxE unlock ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _).
     apply/val_inj => /=; by rewrite inordK.
   rewrite ltnS -ltnNge => n0i; exfalso.
   rewrite -ltnS prednK // in in0'; last by rewrite lt0n.
@@ -234,20 +236,20 @@ rewrite (reindex_onto (@rcs_perm n) (perm_inv (@rcs_perm n))) /=; last first.
   move=> i1 _; by rewrite permKV.
 rewrite (eq_bigl xpredT); last by move=> i1; rewrite permK eqxx.
 apply eq_bigr => i1 _.
-rewrite coef_rVpoly PermDef.fun_of_permE ffunE.
+rewrite coef_rVpoly unlock ffunE.
 case: ifPn => [/eqP ->|].
   case: insubP => [j _ jn0|]; last by rewrite ltnS leqnn.
   rewrite /= in jn0.
   rewrite coef_rVpoly; case: insubP => // k _ k0.
   rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly.
-  rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE k0 /= expr0 mulr1.
+  rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE k0 /= expr0 mulr1.
   by rewrite exprAC an1 expr1n mulr1; congr (x _ _); apply val_inj => /=.
 case: insubP => /= [j|].
   rewrite ltnS => i1n0 ji1 i10; rewrite coef_rVpoly.
   case: insubP => /= [k|].
     rewrite ltnS => i1n0' ki1.
     rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly.
-    rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10).
+    rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10).
     rewrite inordK; last by rewrite ltnW // ltnS prednK // lt0n.
     rewrite prednK // ?lt0n //; congr (x _ _ * _).
     by apply/val_inj.
diff --git a/ecc_classic/decoding.v b/ecc_classic/decoding.v
index 01d1c89c..351d21f5 100644
--- a/ecc_classic/decoding.v
+++ b/ecc_classic/decoding.v
@@ -131,7 +131,7 @@ Section maximum_likelihood_decoding_prop.
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
 Variable repair : decT B [finType of 'rV[A]_n] n.
-Let P := fdist_uniform_supp real_realType (vspace_not_empty C).
+Let P := fdist_uniform_supp R (vspace_not_empty C).
 Hypothesis ML_dec : ML_decoding W C repair P.
 
 Local Open Scope channel_code_scope.
@@ -288,7 +288,7 @@ Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
 Variable dec : decT B [finType of 'rV[A]_n] n.
 Variable dec_img : oimg dec \subset C.
-Let P := fdist_uniform_supp real_realType (vspace_not_empty C).
+Let P := fdist_uniform_supp R (vspace_not_empty C).
 
 Lemma MAP_implies_ML : MAP_decoding W C dec P -> ML_decoding W C dec P.
 Proof.
diff --git a/ecc_classic/hamming_code.v b/ecc_classic/hamming_code.v
index 3cafee7e..d0f34929 100644
--- a/ecc_classic/hamming_code.v
+++ b/ecc_classic/hamming_code.v
@@ -1,8 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
+From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm zmodp.
 From mathcomp Require Import matrix mxalgebra vector.
-From mathcomp Require Import Rstruct.
+From mathcomp Require Import Rstruct reals.
 Require Import realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming.
 Require Import bigop_ext fdist proba channel channel_code decoding.
 Require Import binary_symmetric_channel.
@@ -78,13 +78,13 @@ rewrite /n /len !expnS -subn1 doubleB -muln2 -subSn; last first.
 by rewrite -muln2 mul1n subn2 /= mulnC.
 Qed.
 
-Lemma two_len : 2 < n.
+Lemma two_len : (2 < n)%N.
 Proof. by rewrite len_dim -subn1 ltn_subRL (@leq_exp2l 2 2). Qed.
 
-Lemma dim_len : m <= n.
+Lemma dim_len : (m <= n)%N.
 Proof. by rewrite len_dim -ltnS prednK ?expn_gt0 // ltn_expl. Qed.
 
-Lemma len_two_m (i : 'I_n) : i.+1 < 2 ^ m.
+Lemma len_two_m (i : 'I_n) : (i.+1 < 2 ^ m)%N.
 Proof.
 by rewrite (leq_ltn_trans (ltn_ord i)) // len_dim -ltnS prednK // expn_gt0.
 Qed.
@@ -216,9 +216,9 @@ Proof.
 move: (min_dist_is_min hamming_not_trivial) => Hforall.
 move: (min_dist_achieved hamming_not_trivial) => Hexists.
 move: (min_dist_neq0) => H3.
-suff : min_dist hamming_not_trivial <> 1%N /\
-       min_dist hamming_not_trivial <> 2%N /\
-       min_dist hamming_not_trivial <= 3%N.
+suff : (min_dist hamming_not_trivial <> 1 /\
+       min_dist hamming_not_trivial <> 2 /\
+       min_dist hamming_not_trivial <= 3)%N.
   move : H3.
   move/(_ _ _ _ hamming_not_trivial).
   destruct (min_dist hamming_not_trivial) as [|p]=> //.
@@ -253,7 +253,7 @@ Definition hamming_err y :=
   let i := nat_of_rV (syndrome (Hamming.PCM m) y) in
   if i is O then 0 else rV_of_nat n (2 ^ (n - i)).
 
-Lemma wH_hamming_err_ub y : wH (hamming_err y) <= 1.
+Lemma wH_hamming_err_ub y : (wH (hamming_err y) <= 1)%N.
 Proof.
 rewrite /hamming_err.
 move Hy : (nat_of_rV _) => [|p /=].
@@ -266,13 +266,13 @@ Definition alt_hamming_err (y : 'rV_n) : 'rV['F_2]_n :=
   let n0 := nat_of_rV s in
   if n0 is O then 0 else (\row_(j < n) if n0.-1 == j then 1 else 0).
 
-Lemma alt_hamming_err_ub y : wH (alt_hamming_err y) <= 1.
+Lemma alt_hamming_err_ub y : (wH (alt_hamming_err y) <= 1)%N.
 Proof.
 rewrite /alt_hamming_err.
 destruct (nat_of_rV _); first by rewrite wH0.
 clearbody n; clear.
 rewrite wH_sum.
-case/boolP : (n0 < n) => n0n.
+case/boolP : (n0 < n)%N => n0n.
   rewrite (bigD1 (Ordinal n0n)) //= mxE eqxx (eq_bigr (fun x => O)); last first.
     move=> i Hi; rewrite mxE ifF //.
     apply: contraNF Hi => /eqP Hi; by apply/eqP/val_inj.
@@ -291,7 +291,7 @@ case/boolP : (s == 0) => [/eqP ->|s0].
 have [k ks] : exists k : 'I_n, nat_of_rV s = k.+1.
   move: s0; rewrite -nat_of_rV_eq0 -lt0n => s0.
   move: (nat_of_rV_up s) => sup.
-  have sn1up : (nat_of_rV s).-1 < n.
+  have sn1up : ((nat_of_rV s).-1 < n)%N.
     by rewrite /n Hamming.len_dim -ltnS prednK // prednK // expn_gt0.
   exists (Ordinal sn1up); by rewrite /= prednK.
 rewrite ks /= /syndrome.
@@ -369,13 +369,13 @@ Variable m' : nat.
 Let m := m'.+2.
 Let n := Hamming.len m'.
 
-Lemma cols_PCM : [set c | wH c^T >= 1] = [set col i (Hamming.PCM m) | i : 'I_n].
+Lemma cols_PCM : [set c | (wH c^T >= 1)%N] = [set col i (Hamming.PCM m) | i : 'I_n].
 Proof.
 apply/setP => i.
 rewrite in_set.
-case Hi : (0 < wH i^T).
+case Hi : (0 < wH i^T)%N.
   apply/esym/imsetP.
-  have H0 : nat_of_rV i^T - 1 < n.
+  have H0 : (nat_of_rV i^T - 1 < n)%N.
     have iup := nat_of_rV_up i^T.
     rewrite /n Hamming.len_dim -subn1 ltn_sub2r //.
     by rewrite -{1}(expn0 2) ltn_exp2l // ltnW.
@@ -436,14 +436,14 @@ rewrite !mxE eqxx /=.
 by case Hji : (j == i) => // _; apply/esym/eqP.
 Qed.
 
-Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1].
+Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1]%N.
 
 Definition unit_cols := [set c : 'cV['F_2]_m | wH c^T == 1%nat].
 
 Lemma card_all_cols : #|non_unit_cols :|: unit_cols| = n.
 Proof.
 rewrite /non_unit_cols /unit_cols.
-transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1%nat]|.
+transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1]%N|.
   apply eq_card=> c; by rewrite !in_set orbC eq_sym -leq_eqVlt.
 by rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj.
 Qed.
@@ -521,7 +521,7 @@ Qed.
 Lemma idsA_ids1 (i : 'I_(n - m)) (j : 'I_m) : idsA `_ i <> sval (ids1 j).
 Proof.
 destruct (ids1 j) => /= Hij.
-have Hlti : i < size idsA by rewrite size_idsA.
+have Hlti : (i < size idsA)%N by rewrite size_idsA.
 move: (mem_nth 0 Hlti).
 rewrite Hij => Hi.
 move: (imset_f (fun i => col i (Hamming.PCM m)) Hi).
@@ -571,7 +571,7 @@ Lemma PCM_A_1 : PCM = castmx (erefl, subnK (Hamming.dim_len m')) (row_mx CSM 1).
 Proof.
 apply/matrixP => i j.
 rewrite mxE castmxE /=.
-case/boolP : (j < n - m) => Hcond.
+case/boolP : (j < n - m)%N => Hcond.
   have -> : cast_ord (esym (subnK (Hamming.dim_len m'))) j =
            lshift m (Ordinal Hcond) by apply val_inj.
   rewrite row_mxEl [in X in _  = X]mxE.
@@ -792,7 +792,7 @@ rewrite -mulmxA.
 have [Y1 [Y2 HY]] : exists (Y1 : 'cV_ _) Y2, (row_perm systematic y^T) =
   castmx (subnK (Hamming.dim_len m'), erefl 1%nat) (col_mx Y1 Y2).
   exists (\matrix_(j < 1, i < n - m) (y j (systematic (widen_ord (leq_subr m n) i))))^T.
-  have dim_len_new i (Hi : i < m) : n - m + i < n.
+  have dim_len_new i (Hi : (i < m)%N) : (n - m + i < n)%N.
     by rewrite -ltn_subRL subnBA ?Hamming.dim_len // addnC addnK.
   exists (\matrix_(j < 1, i < m) (y j (systematic (Ordinal (dim_len_new _ (ltn_ord i))))))^T.
   apply/colP => a /=.
@@ -910,7 +910,7 @@ move=> ->.
 Defined.
 
 Lemma encode_decode c y : c \in lcode ->
-  repair y != None -> dH c y <= 1 -> repair y = Some c.
+  repair y != None -> (dH c y <= 1)%N -> repair y = Some c.
 Proof.
 move=> Hc Hy cy.
 apply: (@mddP _ _ lcode _ decoder (hamming_not_trivial r')) => //.
@@ -919,7 +919,7 @@ by rewrite /mdd_err_cor hamming_min_dist.
 Qed.
 
 Lemma repair_failure2 e c : c \in lcode ->
-  ~~ (if repair e is Some y0 then y0 != c else true) -> wH (c + e) <= 1.
+  ~~ (if repair e is Some y0 then y0 != c else true) -> (wH (c + e) <= 1)%N.
 Proof.
 move=> Hc H.
 suff : dH e c = O \/ dH e c = 1%N by rewrite dHE F2_mx_opp addrC; case=> ->.
@@ -933,7 +933,7 @@ rewrite dH_wH leq_eqVlt ?ltnS ?leqn0 => /orP[|] /eqP ->; by auto.
 Qed.
 
 Lemma repair_failure1 e c : c \in lcode ->
-  (if repair e is Some x then x != c else true) -> 1 < wH (c + e).
+  (if repair e is Some x then x != c else true) -> (1 < wH (c + e))%N.
 Proof.
 move=> Hc.
 move xc : (repair e) => [x ex |]; last first.
@@ -947,7 +947,7 @@ rewrite leq_eqVlt ltnS leqn0 orbC => /orP[|/eqP cy1].
 Qed.
 
 Lemma repair_failure e c : c \in lcode ->
-  (if repair e is Some x then x != c else true) = (1 < wH (c + e)).
+  (if repair e is Some x then x != c else true) = (1 < wH (c + e))%N.
 Proof.
 move=> Hc.
 apply/idP/idP; first by move/repair_failure1; apply.
@@ -963,7 +963,7 @@ Require Import Reals Reals_ext.
 Section hamming_code_error_rate.
 
 Variable M : finType.
-Hypothesis M_not_0 : 0 < #|M|.
+Hypothesis M_not_0 : (0 < #|M|)%nat.
 Variable p : {prob R}.
 Let card_F2 : #| 'F_2 | = 2%N. by rewrite card_Fp. Qed.
 Let W := BSC.c card_F2 p.
diff --git a/ecc_classic/linearcode.v b/ecc_classic/linearcode.v
index 31fa4028..e0fa83a8 100644
--- a/ecc_classic/linearcode.v
+++ b/ecc_classic/linearcode.v
@@ -1,5 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg poly polydiv fingroup perm.
 From mathcomp Require Import finalg zmodp matrix mxalgebra mxpoly vector.
 Require Import ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code.
@@ -117,18 +118,23 @@ Proof. by rewrite /syndrome trmx0 mulmx0 trmx0. Qed.
 Lemma additive_syndrome : additive syndrome.
 Proof. move=> x y; by rewrite syndromeD syndromeN. Qed.
 
-Definition lin_syndrome : {linear 'rV[F]_n -> 'rV[F]_m} :=
-  GRing.Linear.Pack _ (GRing.Linear.Class additive_syndrome syndromeZ).
+HB.instance Definition _ :=
+  GRing.isAdditive.Build _ _ _ additive_syndrome.
+HB.instance Definition _ :=
+  GRing.isScalable.Build _ _ _ _ _ syndromeZ.
 
-Definition hom_syndrome : 'Hom(matrix_vectType F 1 n, matrix_vectType F 1 m) :=
-  linfun lin_syndrome.
+(*Definition lin_syndrome : {linear 'rV[F]_n -> 'rV[F]_m} :=
+  GRing.Linear.Pack _ (GRing.Linear.Class additive_syndrome syndromeZ).*)
+
+Definition hom_syndrome : 'Hom('rV[F]_n, 'rV[F]_m) :=
+  linfun syndrome.
 
 Definition kernel : Lcode0.t F n := lker hom_syndrome.
 
 Lemma dim_hom_syndrome_ub : \dim (limg hom_syndrome) <= m.
 Proof.
 rewrite [in X in _ <= X](_ : m = \dim (fullv : {vspace 'rV[F]_m})); last first.
-  by rewrite dimvf /Vector.dim /= mul1n.
+  by rewrite dimvf/= /dim/= mul1n.
 by rewrite dimvS // subvf.
 Qed.
 
@@ -139,7 +145,7 @@ Lemma dim_kernel (Hm : \rank H = m) (mn : m <= n) : \dim kernel = (n - m)%N.
 Proof.
 move: (limg_ker_dim hom_syndrome fullv).
 rewrite (_ : (fullv :&: _)%VS = kernel); last by apply/capv_idPr/subvf.
-rewrite (_ : \dim fullv = n); last by rewrite dimvf /Vector.dim /= mul1n.
+rewrite (_ : \dim fullv = n); last by rewrite dimvf /dim /= mul1n.
 move=> H0; rewrite -{}[in RHS]H0.
 suff -> : \dim (limg hom_syndrome) = m by rewrite addnK.
 set K := castmx (erefl, Hm) (col_base H).
@@ -190,14 +196,14 @@ Section dual_code.
 Variables (F : finFieldType) (m n : nat) (H : 'M[F]_(m, n)).
 
 Definition dual_code : {vspace 'rV[F]_n} :=
-  (linfun (mulmxr_linear _ H) @: fullv)%VS.
+  (linfun (mulmxr H) @: fullv)%VS.
 
 Lemma dim_dual_code : (\dim (kernel H) + \dim dual_code = n)%N.
 Proof.
-move: (limg_ker_dim (linfun (lin_syndrome H)) fullv).
+move: (limg_ker_dim (linfun (syndrome H)) fullv).
 rewrite -/(kernel H).
 rewrite (_ : (fullv :&: _)%VS = kernel H); last by apply/capv_idPr/subvf.
-rewrite (_ : \dim fullv = n); last by rewrite dimvf /Vector.dim /= mul1n.
+rewrite (_ : \dim fullv = n); last by rewrite dimvf /dim /= mul1n.
 rewrite (_ : \dim (limg _) = \dim dual_code) // /dual_code.
 rewrite /dimv.
 Abort.
@@ -390,9 +396,14 @@ Proof. by apply/rowP => i; rewrite !mxE. Qed.
 Lemma additive_sbound_f' k (H : k.-1 <= n) : additive (sbound_f' H).
 Proof. by move=> x y; rewrite sbound_f'D sbound_f'N. Qed.
 
-Definition sbound_f_linear k (H : k.-1 <= n) :
+HB.instance Definition _ k (H : k.-1 <= n) :=
+  GRing.isAdditive.Build _ _ _ (additive_sbound_f' H).
+HB.instance Definition _ k (H : k.-1 <= n) :=
+  GRing.isScalable.Build _ _ _ _ _ (sbound_f'Z H).
+
+(*Definition sbound_f_linear k (H : k.-1 <= n) :
   {linear 'rV[F]_n -> 'rV[F]_k.-1} :=
-  GRing.Linear.Pack _ (GRing.Linear.Class (additive_sbound_f' H) (sbound_f'Z H)).
+  GRing.Linear.Pack _ (GRing.Linear.Class (additive_sbound_f' H) (sbound_f'Z H)).*)
 
 (* McEliece, theorem 9.8, p.255 *)
 Lemma singleton_bound : min_dist <= n - \dim C + 1.
@@ -400,18 +411,18 @@ Proof.
 set k := \dim C.
 have dimCn : k.-1 < n.
   have /dimvS := subvf C.
-  rewrite dimvf /Vector.dim /= mul1n.
+  rewrite dimvf /dim /= mul1n.
   by apply: leq_trans; rewrite prednK // not_trivial_dim.
-set f := linfun (sbound_f_linear (ltnW dimCn)).
+set f := linfun (sbound_f' (ltnW dimCn)).
 have H1 : \dim (f @: C) <= k.-1.
   suff : \dim (f @: C) <= \dim (fullv : {vspace 'rV[F]_k.-1}).
-    by rewrite dimvf /= /Vector.dim /= mul1n.
+    by rewrite dimvf /= /dim /= mul1n.
   by apply/dimvS/subvf.
 have H2 : (\dim (f @: C) + \dim (C :&: lker f) = \dim (fullv : {vspace 'rV[F]_k}))%N.
-  by rewrite dimvf /= /Vector.dim /= mul1n -[RHS](limg_ker_dim f C) addnC.
+  by rewrite dimvf /= /dim /= mul1n -[RHS](limg_ker_dim f C) addnC.
 have H3 : 1 <= \dim (C :&: lker f).
   rewrite lt0n; apply/eqP => abs; move: H2.
-  rewrite abs addn0 dimvf /Vector.dim /= mul1n -/k.
+  rewrite abs addn0 dimvf /dim /= mul1n -/k.
   apply/eqP.
   move: H1; rewrite leqNgt; apply: contra => /eqP ->.
   by rewrite prednK // not_trivial_dim.
diff --git a/ecc_modern/checksum.v b/ecc_modern/checksum.v
index 1b4ca63c..bf408140 100644
--- a/ecc_modern/checksum.v
+++ b/ecc_modern/checksum.v
@@ -1,8 +1,9 @@
 (* infotheo: information theory and error-correcting codes in Coq               *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later              *)
-From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
+From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm zmodp.
 From mathcomp Require Import matrix vector.
 Require Import Reals.
+From mathcomp Require Import Rstruct.
 Require Import ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode.
 Require Import pproba.
 
@@ -171,7 +172,7 @@ Qed.
 Local Close Scope R_scope.
 
 Let C := kernel H.
-Hypothesis HC : 0 < #| [set cw in C] |.
+Hypothesis HC : (0 < #| [set cw in C] |)%nat.
 
 Local Open Scope proba_scope.
 Variable y : (`U HC).-receivable W.
diff --git a/ecc_modern/degree_profile.v b/ecc_modern/degree_profile.v
index 5167a9ff..9256b446 100644
--- a/ecc_modern/degree_profile.v
+++ b/ecc_modern/degree_profile.v
@@ -1,5 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
 From mathcomp Require Import matrix perm.
 From mathcomp Require boolp.
@@ -119,8 +120,7 @@ Proof.
 by move=> [] []; constructor.
 Qed.
 
-Canonical kind_eqMixin := EqMixin kind_eqP.
-Canonical kind_eqType := Eval hnf in EqType _ kind_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ kind_eqP.
 
 Definition negk k := if k is kv then kf else kv.
 Lemma negk_involution k : negk (negk k) = k.
@@ -189,11 +189,9 @@ elim: l k => [|l IH] k t.
 Qed.
 End EncodeDecode.
 
-Definition tree_eqMixin l k := CanEqMixin (@cancel_tree l k).
-Canonical tree_eqType l k := Eval hnf in EqType _ (@tree_eqMixin l k).
-Definition tree_choiceMixin l k := CanChoiceMixin (@cancel_tree l k).
-Canonical tree_choiceType l k :=
-  Eval hnf in ChoiceType _ (tree_choiceMixin l k).
+HB.instance Definition _ l k := Equality.copy (tree l k) (can_type (@cancel_tree l k)).
+
+HB.instance Definition _ l k := Choice.copy (tree l k) (can_type (@cancel_tree l k)).
 
 (* For finite types we need to limit the branching degree *)
 Fixpoint max_deg (l : nat) k (t : tree l k) : nat :=
@@ -267,17 +265,13 @@ congr mkFintree.
 by apply eq_irrelevance.
 Qed.
 
-Definition fintree_eqMixin n l := CanEqMixin (@cancel_fintree n l).
-Canonical fintree_eqType n l := Eval hnf in EqType _ (@fintree_eqMixin n l).
-Definition fintree_choiceMixin n l := CanChoiceMixin (@cancel_fintree n l).
-Canonical fintree_choiceType n l := Eval hnf in
-      ChoiceType _ (fintree_choiceMixin n l).
+HB.instance Definition _ n l := Equality.copy (fintree n l) (can_type (@cancel_fintree n l)).
+
+HB.instance Definition _ n l := Choice.copy (fintree n l) (can_type (@cancel_fintree n l)).
 
-Definition tree_countMixin l k := CanCountMixin (@cancel_tree l k).
-Canonical tree_countType l k := Eval hnf in CountType _ (tree_countMixin l k).
-Definition fintree_countMixin n l := CanCountMixin (@cancel_fintree n l).
-Canonical fintree_countType n l := Eval hnf in
-      CountType _ (fintree_countMixin n l).
+HB.instance Definition _ l k := Countable.copy (tree l k) (can_type (@cancel_tree l k)).
+
+HB.instance Definition _ n l := Countable.copy (fintree n l) (can_type (@cancel_fintree n l)).
 
 Section count_allpairs.
 
@@ -446,9 +440,7 @@ have /mapP [x Hx1 Hx2]  : ft t \in [seq ft i | i <- s].
 by rewrite (can_inj (@cancel_fintree n l) Hx2) Hx1.
 Qed.
 
-Definition fintree_finMixin n l := Eval hnf in FinMixin (@fintree_enumP n l).
-
-Canonical fintree_finType n l := Eval hnf in FinType _ (fintree_finMixin n l).
+HB.instance Definition _ n l := @isFinite.Build (fintree n l) _ (@fintree_enumP n l).
 
 Local Open Scope fdist_scope.
 
@@ -638,8 +630,7 @@ Qed.
 Lemma f1 l : \sum_(t : @fintree tw l) (@fintree_dist l t) = 1.
 Proof.
 rewrite /index_enum /=.
-have ->: Finite.enum (fintree_finType tw l)
-    = fintree_enum tw l.
+have ->: Finite.enum (fintree tw l) = fintree_enum tw l.
   by rewrite unlock /=.
 rewrite /fintree_enum.
 destruct (fintree_enum_dep _ _) => /=.
@@ -1117,9 +1108,7 @@ apply ReflectF => [] [].
 by move/Hp.
 Qed.
 
-Definition hemi_comp_graph_eqMixin := EqMixin hemi_comp_graph_eqP.
-Canonical hemi_comp_graph_eqType :=
-  Eval hnf in EqType _ hemi_comp_graph_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ hemi_comp_graph_eqP.
 
 Definition comp_graph_eqb (c1 c2 : comp_graph) :=
  [&& nodes c1 == nodes c2, conodes c1 == conodes c2 & edges c1 == edges c2].
@@ -1147,9 +1136,7 @@ apply ReflectF => [] [].
 by move/Hn.
 Qed.
 
-Definition comp_graph_eqMixin := EqMixin comp_graph_eqP.
-Canonical comp_graph_eqType :=
-  Eval hnf in EqType _ comp_graph_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ comp_graph_eqP.
 
 End pcomp_graph_def.
 
@@ -1195,7 +1182,7 @@ case: ifP => Hend.
     by rewrite (subsetP (border_p (conodes c)) _ Hx2) orbT.
   apply/orP; left.
   apply/bigcupP; exists end_node; last by [].
-  by rewrite in_set eqxx.
+  by rewrite inE eqxx.
 Qed.
 
 Definition step_conodes : hemi_comp_graph port :=
diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v
index 539f9f76..dfdf1463 100644
--- a/ecc_modern/ldpc_algo.v
+++ b/ecc_modern/ldpc_algo.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
+From HB Require Import structures.
 Require Import Init.Wf Recdef Reals.
-From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
+From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg ssrnum.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext f2 subgraph_partition tanner.
 Require Import fdist channel pproba linearcode ssralg_ext.
@@ -79,7 +80,18 @@ Definition alpha_op (out inp : R2) :=
   (o*i + o'*i', o*i' + o'*i).
 Definition alpha := foldr alpha_op (1,0).
 
-Program Definition alpha_op_monoid_law : Monoid.law (R1, R0) := @Monoid.Law _ _ alpha_op _ _ _.
+Lemma alphaA : associative alpha_op.
+Proof. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; f_equal; ring. Qed.
+
+Lemma alphaC : commutative alpha_op.
+Proof. by move=> -[a0 a1] [b0 b1]/=; f_equal; ring. Qed.
+
+Lemma alpha0x : left_id (R1, R0) alpha_op.
+Proof. by move=> -[a0 a1] /=; f_equal; ring. Qed.
+
+HB.instance Definition _ := @Monoid.isComLaw.Build _ _ _ alphaA alphaC alpha0x.
+
+(*Program Definition alpha_op_monoid_law : Monoid.law (R1, R0) := @Monoid.Law _ _ alpha_op _ _ _.
 Next Obligation. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; f_equal; ring. Qed.
 Next Obligation. by move=> -[a0 a1] /=; f_equal; ring. Qed.
 Next Obligation. by move=> -[a0 a1] /=; f_equal; ring. Qed.
@@ -87,7 +99,7 @@ Canonical alpha_op_monoid_law.
 
 Program Definition alpha_op_monoid_com_law := @Monoid.ComLaw R2 _ alpha_op_monoid_law _.
 Next Obligation. by move=> -[a0 a1] [b0 b1] /=; f_equal; ring. Qed.
-Canonical alpha_op_monoid_com_law.
+Canonical alpha_op_monoid_com_law.*)
 
 (** β[m0,n0](x) = W(y_n0|x) Π_{m1 ∈ F(n0)\{m0}} α[m1,n0](x) *)
 
@@ -96,7 +108,18 @@ Definition beta_op (out inp : R2) :=
   let (o,o') := out in let (i,i') := inp in (o*i, o'*i').
 Definition beta := foldl beta_op.
 
-Program Definition beta_op_monoid_law : Monoid.law (R1, R1) := @Monoid.Law _ _ beta_op _ _ _.
+Lemma betaA : associative beta_op.
+Proof. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; f_equal; ring. Qed.
+
+Lemma betaC : commutative beta_op.
+Proof. by move=> -[a0 a1] [b0 b1]/=; f_equal; ring. Qed.
+
+Lemma beta0x : left_id (R1, R1) beta_op.
+Proof. by move=> -[a0 a1] /=; f_equal; ring. Qed.
+
+HB.instance Definition _ := @Monoid.isComLaw.Build _ _ _ betaA betaC beta0x.
+
+(*Program Definition beta_op_monoid_law : Monoid.law (R1, R1) := @Monoid.Law _ _ beta_op _ _ _.
 Next Obligation. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; rewrite !mulRA. Qed.
 Next Obligation. by move=> -[a0 a1]; rewrite /beta_op !mul1R. Qed.
 Next Obligation. by move=> -[a0 a1]; rewrite /beta_op !mulR1. Qed.
@@ -104,7 +127,7 @@ Canonical beta_op_monoid_law.
 
 Program Definition beta_op_monoid_com_law : Monoid.com_law (R1, R1) := @Monoid.ComLaw _ _ beta_op_monoid_law _.
 Next Obligation. by move=> -[a0 a1] [b0 b1]; rewrite /beta_op /= (mulRC a0) (mulRC a1). Qed.
-Canonical beta_op_monoid_com_law.
+Canonical beta_op_monoid_com_law.*)
 
 (** Select α or β according to node kind *)
 Definition alpha_beta {b} (t : tag b) :=
diff --git a/ecc_modern/ldpc_algo_proof.v b/ecc_modern/ldpc_algo_proof.v
index c185c8da..d2e5bd87 100644
--- a/ecc_modern/ldpc_algo_proof.v
+++ b/ecc_modern/ldpc_algo_proof.v
@@ -1,7 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
+From HB Require Import structures.
 Require Import Wf_nat Init.Wf Recdef Reals.
-From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
+From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg ssrnum.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2.
 Require Import fdist channel pproba linearcode subgraph_partition tanner.
@@ -45,8 +46,7 @@ Proof.
 by move=> [] []; constructor.
 Qed.
 
-Canonical kind_eqMixin := EqMixin kind_eqP.
-Canonical kind_eqType := Eval hnf in EqType _ kind_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ kind_eqP.
 
 Definition tag_eq_bool k (t1 t2 : tag k) : bool :=
   match t1, t2 with
@@ -71,8 +71,7 @@ Section EqTag.
 
 Variable k : kind.
 
-Canonical tag_eqMixin := EqMixin (@tag_eqP k).
-Canonical tag_eqType := Eval hnf in EqType _ tag_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ (@tag_eqP k).
 
 End EqTag.
 
@@ -126,8 +125,7 @@ Section EqTnTree.
 
 Variable k : kind.
 
-Canonical tn_tree_eqMixin := EqMixin (@tn_tree_eqP k).
-Canonical tn_tree_eqType := Eval hnf in EqType _ tn_tree_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ (@tn_tree_eqP k).
 
 End EqTnTree.
 
@@ -299,7 +297,7 @@ move/(_ (eqxx true)) => Hcy.
 by rewrite (eqP Hcy) Hy in Hch.
 Qed.
 
-Lemma seq_full {A:finType} (s : seq A) a : #|A| - #|s| <= 0 -> a \in s.
+Lemma seq_full {A:finType} (s : seq A) a : (#|A| - #|s| <= 0)%N -> a \in s.
 Proof.
 move=> Hh.
 have Hs: finset (mem s) = [set: A].
@@ -313,7 +311,7 @@ Qed.
 Definition lastE := (last_cat, last_rcons, last_cons).
 
 Lemma card_uniq_seq_decr {T : finType} x (s : seq T) h :
-  #|T| - #|s| <= h.+1 -> uniq (x :: s) -> #|T| - #|x :: s| <= h.
+  (#|T| - #|s| <= h.+1)%N -> uniq (x :: s) -> (#|T| - #|x :: s| <= h)%N.
 Proof.
 move=> Hh Hun.
 move /card_uniqP: (Hun) => ->.
@@ -324,7 +322,7 @@ by move /andP/proj2/card_uniqP: Hun => <-.
 Qed.
 
 Lemma build_tree_rec_ok h k i s :
-  #|id'| - #|s| <= h ->
+  (#|id'| - #|s| <= h)%N ->
   uniq_path (tanner_rel H) (id_of_kind k i) s ->
   let l := labels (build_tree_rec H rW h s k i) in
   forall a b, a \in l -> b \in l ->
@@ -469,7 +467,7 @@ by move /norP/proj2: Hc.
 Qed.
 
 Lemma build_tree_rec_full h k i s :
-  #|id'| - #|s| <= h ->
+  (#|id'| - #|s| <= h)%N ->
   uniq_path (tanner_rel H) (id_of_kind k i) s ->
   mem (labels (build_tree_rec H rW h s k i)) =i
   connect (tanner_split s) (id_of_kind k i).
@@ -485,7 +483,7 @@ case Hai: (a == id_of_kind k i); simpl.
   apply /connectP.
   by exists [::].
 move/andP: Hc => [] /= Hc Hun.
-have Hh': #|id'| - #|id_of_kind k i :: s| <= h.
+have Hh': (#|id'| - #|id_of_kind k i :: s| <= h)%N.
   by apply card_uniq_seq_decr.
 have Hchild o: o \in select_children H s k i ->
   uniq_path (tanner_rel H) (id_of_kind (negk k) o) (id_of_kind k i :: s).
@@ -638,7 +636,7 @@ Fixpoint mypath (h : nat) : seq (seq id') :=
   end.
 
 Theorem test_acyclic : forall p, p \in [::] :: mypath (m+n) ->
-                                (size p > 2) ==> ~~ ucycleb myrel p.
+                                (size p > 2)%N ==> ~~ ucycleb myrel p.
 Proof. by apply /allP. Qed.
 
 Lemma myrel_ok : myrel =2 tanner_rel H.
@@ -656,7 +654,7 @@ elim: h a => [|h Hh] a.
   by rewrite ltn0.
 rewrite /= in_cons.
 case/boolP : (_ == _) => //= a_not_h.
-suff a_ltn_h : a < h.
+suff a_ltn_h : (a < h)%N.
   apply/mapP.
   exists (Ordinal a_ltn_h) => //.
   by apply val_inj.
@@ -670,7 +668,7 @@ destruct a; [left | right]; apply /map_f/my_ord_enum_ok.
 Qed.
 
 Lemma mypath_ok_rec h a p :
-  (size p) < h -> path myrel a p -> (a :: p \in mypath h).
+  (size p < h)%N -> path myrel a p -> (a :: p \in mypath h).
 Proof.
 elim: h a p => [//|h IHh] a p Hp Hun.
 suff : a :: p \in flatten [seq [seq i :: l |
@@ -692,7 +690,7 @@ Lemma mypath_ok a p :
   uniq (a :: p) -> path myrel a p -> (a :: p) \in mypath (m+n).
 Proof.
 move /card_uniqP => Hsz Hp.
-have Hc: #|a::p| <= #|id'| by apply max_card.
+have Hc : (#|a::p| <= #|id'|)%N by apply max_card.
 rewrite Hsz card_sum !card_ord in Hc.
 by apply mypath_ok_rec.
 Qed.
@@ -1835,11 +1833,14 @@ case Hid: (node_id t == inr n0).
     rewrite set1F -imset_set1 (kind_filter (k:=kv)).
     rewrite !beta_map -Monoid.mulmA; congr beta_op.
     rewrite big_filter (eq_bigr (fun j => msg_spec' (inl j) (inr i))) //.
-    rewrite Monoid.mulmC -big_filter.
+    set tmp := alpha_beta _ _.
+    rewrite /=.
+    rewrite Monoid.mulmC -big_filter/=.
+    rewrite /tmp.
     rewrite -msg_spec_alpha_beta; last first.
       rewrite sym_tanner_rel.
       by move/andP/proj1: Hun => /= /andP/proj1.
-    rewrite -(big_seq1 beta_op_monoid_law o (fun j => msg_spec' (inl j) (inr i))).
+    rewrite -(big_seq1 beta_op o (fun j => msg_spec' (inl j) (inr i))).
     rewrite -big_cat.
     apply/perm_big/uniq_perm.
      - rewrite /= filter_uniq.
diff --git a/ecc_modern/ldpc_erasure.v b/ecc_modern/ldpc_erasure.v
index 458c6933..c03525cf 100644
--- a/ecc_modern/ldpc_erasure.v
+++ b/ecc_modern/ldpc_erasure.v
@@ -1,5 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
+From HB Require Import structures.
 Require Program.Wf.
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix.
@@ -57,8 +58,7 @@ case: a b; [|by case|by case].
 by move=> a'; case => //= b' /eqP ->.
 Qed.
 
-Canonical letter_eqMixin := EqMixin eqlP.
-Canonical letter_eqType := Eval hnf in EqType letter letter_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ eqlP.
 
 CoInductive letter_spec : letter -> bool -> bool -> bool -> bool -> Prop :=
 | letter_spec0 : letter_spec (Bit 0) true false false false
@@ -91,17 +91,12 @@ Definition letter_unpickle (n : nat) :=
 Lemma letter_count : pcancel letter_pickle letter_unpickle.
 Proof. by case/letterP. Qed.
 
-Definition letter_choiceMixin := PcanChoiceMixin letter_count.
-Canonical letter_choiceType := Eval hnf in ChoiceType letter letter_choiceMixin.
-
-Definition letter_countMixin := PcanCountMixin letter_count.
-Canonical letter_countType := Eval hnf in CountType letter letter_countMixin.
+HB.instance Definition _ := @PCanIsCountable _ _ _ _ letter_count.
 
 Lemma letter_enumP : Finite.axiom [::Bit 0; Bit 1; Star; Blank].
 Proof. by case => //; case/F2P. Qed.
 
-Definition letter_finMixin := Eval hnf in FinMixin letter_enumP.
-Canonical letter_finType := Eval hnf in FinType letter letter_finMixin.
+HB.instance Definition _ := @isFinite.Build letter _ letter_enumP.
 
 Definition F2_of_letter (l : letter) : 'F_2 := if l is Bit a then a else 0.
 
diff --git a/ecc_modern/summary.v b/ecc_modern/summary.v
index f678a699..197cc138 100644
--- a/ecc_modern/summary.v
+++ b/ecc_modern/summary.v
@@ -208,12 +208,13 @@ transitivity (\sum_(f in {ffun 'I_n -> bool} | freeon s d (\row_i F2_of_bool (f
   by rewrite 2!tnth_fgraph ffunE.
 transitivity (\sum_(f in {set 'I_n} | freeon s d (\row_i F2_of_bool (i \in f)))
       e (\row_k0 (if k0 \in s then F2_of_bool (k0 \in f) else d ``_ k0)))%R.
-  rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [set x | f x ])
-    (@finfun_of_set [finType of 'I_n])).
+  have @f' : {set 'I_n} -> {ffun 'I_n -> bool} := (fun x => [ffun i => i \in x]).
+  rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [set x | f x ]) f').
     apply eq_big => /= f.
       rewrite -[LHS]andbT; congr (freeon s d _ && _).
-        apply/rowP => i; by rewrite !mxE inE.
-      apply/esym/eqP/ffunP => /= i; by rewrite SetDef.finsetE ffunE.
+        by apply/rowP => i; rewrite !mxE inE.
+      apply/esym/eqP/ffunP => /= i.
+      by rewrite /f' ffunE inE.
     move=> Hf.
     congr e.
     apply/rowP => b; rewrite !mxE.
@@ -221,8 +222,7 @@ transitivity (\sum_(f in {set 'I_n} | freeon s d (\row_i F2_of_bool (i \in f)))
     by rewrite inE tnth_fgraph -enum_rank_ord enum_rankK.
   move=> /= f Hf.
   apply/setP => /= k0.
-  rewrite inE.
-  by rewrite SetDef.pred_of_setE.
+  by rewrite inE /f' ffunE.
 transitivity (\sum_(f in {set 'I_n} | f \subset s) e (\row_(k0 < n) if k0 \in s then F2_of_bool (k0 \in f) else d ``_ k0))%R; last first.
   apply eq_bigl => /= s0.
   by rewrite powersetE.
diff --git a/ecc_modern/summary_tanner.v b/ecc_modern/summary_tanner.v
index b7462b33..42465fb5 100644
--- a/ecc_modern/summary_tanner.v
+++ b/ecc_modern/summary_tanner.v
@@ -1,6 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq               *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later              *)
-From mathcomp Require Import all_ssreflect ssralg fingroup finalg zmodp matrix.
+From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg zmodp matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
 Require Import ssr_ext ssralg_ext ssrR Reals_ext f2 summary.
diff --git a/ecc_modern/tanner.v b/ecc_modern/tanner.v
index 48772264..73d57a27 100644
--- a/ecc_modern/tanner.v
+++ b/ecc_modern/tanner.v
@@ -121,9 +121,9 @@ Lemma Vgraph_set1 m1 n1 : n1 \notin 'V m1 -> 'V(m1, n1) = [set n1].
 Proof.
 move=> m1n1.
 apply/setP => n2.
-rewrite inE in_set1 /=.
+rewrite !inE.
 case/boolP: (n2 == n1) => //= n2n1.
-by rewrite 2!inE -VnextE (negbTE m1n1).
+by rewrite -VnextE (negbTE m1n1).
 Qed.
 
 (** Function nodes *)
diff --git a/ecc_modern/tanner_partition.v b/ecc_modern/tanner_partition.v
index 0f1e9386..95b390ce 100644
--- a/ecc_modern/tanner_partition.v
+++ b/ecc_modern/tanner_partition.v
@@ -975,8 +975,7 @@ move/negbT : Hlhs; apply contra.
 case/andP.
 rewrite 2!inE.
 move=> n1n0.
-rewrite in_set1 (negbTE n1n0) orFb.
-rewrite inE.
+rewrite !inE (negbTE n1n0) orFb.
 case/andP => _ Hn1.
 apply/bigcupP => /=.
 case/connectP : Hn1 => /= p.
@@ -1013,7 +1012,7 @@ exists m1.
   by apply: contra Hun => /eqP ->.
 rewrite !inE (negbTE n1n2) /= -VnextE -FnextE.
 case/andP : H2 => -> H2 /=.
-apply/connectP; exists p' => //.
+apply/connectP; exists p'; last by [].
 apply: sub_path_except H3 => //.
 apply/negP => n2p'.
 move: Hun.
diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v
index fc58c527..00434e75 100644
--- a/information_theory/channel_coding_direct.v
+++ b/information_theory/channel_coding_direct.v
@@ -1,5 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix perm.
 Require Import Reals Lra Classical.
 From mathcomp Require Import Rstruct classical_sets.
@@ -445,7 +446,7 @@ elim: m n F => [m2 F /=|m IH n F].
   apply eq_bigr => // i _; congr F.
   exact/val_inj.
 - symmetry.
-  transitivity (\sum_(p in tuple_finType (m + n).+1 C) F p)%R; first by apply congr_big.
+  transitivity (\sum_(p in [the finType of (m + n).+1.-tuple C]) F p)%R; first by apply congr_big.
   rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT).
   rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT).
   apply eq_bigr => i _.
@@ -749,7 +750,7 @@ have -> : lhs = (#| M |.-1%:R * Pr ((P `^ n) `x ((`O(P , W)) `^ n)) [set x | pro
       case=> H1; by rewrite {1}H1.
     rewrite cardsE.
     apply eq_card => m_.
-    by rewrite -!topredE /= !finset.in_set andbC.
+    by rewrite -!topredE /= !finset.in_set andbC/= inE.
   by apply eq_big => //; exact: second_summand.
 rewrite card_ord /=.
 apply (@leR_ltR_trans (epsilon0 + k%:R *
diff --git a/information_theory/entropy_convex.v b/information_theory/entropy_convex.v
index ad4b4eca..d4957147 100644
--- a/information_theory/entropy_convex.v
+++ b/information_theory/entropy_convex.v
@@ -50,7 +50,7 @@ Import Order.POrderTheory GRing.Theory Num.Theory.
 
 Section entropy_log_div.
 Variables (A : finType) (p : {fdist A}) (n : nat) (An1 : #|A| = n.+1).
-Let u := @fdist_uniform R_numFieldType _ _ An1.
+Let u := @fdist_uniform R _ _ An1.
 
 Local Open Scope divergence_scope.
 
@@ -85,6 +85,10 @@ Implicit Types p q : {prob R}.
 
 Definition dom_pair := {d : {fdist A} * {fdist A} | d.1 `<< d.2}.
 
+(* TODO: wouldn't be needed if dominates were on bool *)
+HB.instance Definition _ := boolp.gen_eqMixin dom_pair.
+HB.instance Definition _ := boolp.gen_choiceMixin dom_pair.
+
 Lemma dom_conv p (x y u v : {fdist A}) :
   x `<< y -> u `<< v -> x <| p |> u `<< y <| p |> v.
 Proof.
@@ -123,7 +127,7 @@ Let avgA p q x y z :
 Proof. by rewrite /avg /=; exact/boolp.eq_exist/convA. Qed.
 
 HB.instance Definition _ := @isConvexSpace.Build dom_pair
-  (Choice.class (choice_of_Type dom_pair)) avg avg1 avgI avgC avgA.
+  avg avg1 avgI avgC avgA.
 
 End dominated_pair.
 
@@ -146,14 +150,16 @@ have [y2a0|y2a0] := eqVneq (y.2 a) 0.
   have [p0|p0] := eqVneq p 0%:pr.
     by rewrite p0 -!RmultE -!RplusE ?(mul0R,mulR0,addR0).
   apply/Req_le; rewrite -!RmultE -!RplusE mulRA ?(mulR0,addR0); congr (_ * _ * log _).
-  simpl.
+  set u := x.1 a.
+  set v := x.2 a.
   by field; split; exact/eqP.
 have [x2a0|x2a0] := eqVneq (x.2 a) 0.
   rewrite x2a0 (_ : x.1 a = 0)// -?RplusE -?RmultE ?(mulR0,add0R,mul0R); last first.
     by move/dominatesP : Hx; exact.
   have [->|t0] := eqVneq (Prob.p p).~ 0; first by rewrite !mul0R.
   apply/Req_le; rewrite mulRA; congr (_ * _ * log _).
-  simpl.
+  set u := y.1 a.
+  set v := y.2 a.
   by field; split; exact/eqP.
 set h : {fdist A} -> {fdist A} -> {ffun 'I_2 -> R} := fun p1 p2 => [ffun i =>
   [eta (fun=> 0) with ord0 |-> Prob.p p * p1 a, lift ord0 ord0 |-> (Prob.p p).~ * p2 a] i].
@@ -203,7 +209,7 @@ Hypothesis cardA_gt0 : (0 < #|A|)%nat.
 Let cardApredS : #|A| = #|A|.-1.+1.
 Proof. by rewrite prednK. Qed.
 
-Lemma entropy_concave : concave_function (fun P : choice_of_Type {fdist A} => `H P).
+Lemma entropy_concave : concave_function (fun P : {fdist A} => `H P).
 Proof.
 apply RNconcave_function => p q t; rewrite /convex_function_at.
 rewrite !(entropy_log_div _ cardApredS) /= /leconv /= [in X in _ <= X]avgRE.
@@ -219,7 +225,7 @@ End entropy_concave.
 
 Module entropy_concave_alternative_proof_binary_case.
 
-Lemma pderivable_H2 : pderivable H2 (CSet.car open_unit_interval).
+Lemma pderivable_H2 : pderivable H2 uniti.
 Proof.
 move=> x /= [Hx0 Hx1].
 apply derivable_pt_plus.
@@ -264,10 +270,10 @@ move=> ? ? ? x [? ?]; split;
 Qed.
 
 Lemma concavity_of_entropy_x_le_y x y (t : {prob R}) :
-  x \in open_unit_interval -> y \in open_unit_interval -> x < y ->
+  uniti x -> uniti y -> x < y ->
   concave_function_at H2 x y t.
 Proof.
-rewrite !classical_sets.in_setE => -[H0x Hx1] [H0y Hy1] Hxy.
+move=> -[H0x Hx1] [H0y Hy1] Hxy.
 apply RNconcave_function_at.
 set Df := fun z : R => log z - log (1 - z).
 have @f_derive : pderivable (fun x0 => - H2 x0) (fun z => x <= z <= y).
@@ -325,7 +331,7 @@ have DDf_nonneg : forall z, x <= z <= y -> 0 <= DDf z.
 exact: (@second_derivative_convexf_pt _ _ _ _ Df _ _ DDf).
 Qed.
 
-Lemma concavity_of_entropy : concave_function_in open_unit_interval H2.
+Lemma concavity_of_entropy : concave_function_in uniti H2.
 Proof.
 rewrite /concave_function_in => x y t Hx Hy.
 apply: RNconcave_function_at.
@@ -342,7 +348,7 @@ wlog : x y Hx Hy Hxy / x < y.
   apply: convex_function_sym => // t0.
   by apply H => //; left.
 move=> Hxy' t.
-exact/R_convex_function_atN /concavity_of_entropy_x_le_y.
+by apply/R_convex_function_atN /concavity_of_entropy_x_le_y => //; apply/classical_sets.set_mem.
 Qed.
 
 End entropy_concave_alternative_proof_binary_case.
@@ -353,10 +359,10 @@ Variables (A B : finType) (W : A -> {fdist B}).
 Hypothesis B_not_empty : (0 < #|B|)%nat.
 
 Lemma mutual_information_concave :
-  concave_function (fun P : choice_of_Type {fdist A} => mutual_info (P `X W)).
+  concave_function (fun P : {fdist A} => mutual_info (P `X W)).
 Proof.
 suff : concave_function
-  (fun P : choice_of_Type {fdist A} => let PQ := fdistX (P `X W) in `H PQ`1 - cond_entropy PQ).
+  (fun P : {fdist A} => let PQ := fdistX (P `X W) in `H PQ`1 - cond_entropy PQ).
   set f := fun _ => _. set g := fun _ => _.
   suff -> : f = g by [].
   by rewrite boolp.funeqE => d; rewrite {}/f {}/g /= -mutual_infoE -mutual_info_sym.
@@ -367,7 +373,7 @@ apply: R_concave_functionB.
   apply: leR_trans (concave_H (p `X W)`2 (q `X W)`2 t).
   under eq_bigr do rewrite fdist_prod2_conv.
   by apply/RleP; rewrite lexx.
-suff : affine (fun x : choice_of_Type {fdist A} => cond_entropy (fdistX (x `X W))).
+suff : affine (fun x : {fdist A} => cond_entropy (fdistX (x `X W))).
   by move=> /affine_functionP[].
 move=> t p q.
 rewrite /= avgRE /cond_entropy /cond_entropy1.
diff --git a/information_theory/error_exponent.v b/information_theory/error_exponent.v
index c878b080..0bbf8dcb 100644
--- a/information_theory/error_exponent.v
+++ b/information_theory/error_exponent.v
@@ -54,8 +54,7 @@ apply/RleP; rewrite -(@ler_pM2r _ (/ 2)); last first.
   by rewrite RinvE' invr_gt0// (_ : 2%coqR = 2%:R)// INRE ltr0n.
 rewrite RmultE -mulrA mulrCA RinvE' (_ : 2%coqR = 2%:R)// INRE.
 rewrite mulfV ?mulr1 ?gt_eqF//.
-  by apply/RleP; rewrite -RdivE'.
-exact/RltP.
+by apply/RleP; rewrite -RdivE'.
 Qed.
 
 Local Open Scope variation_distance_scope.
diff --git a/information_theory/source_coding_fl_direct.v b/information_theory/source_coding_fl_direct.v
index eb3edf4a..e15eba93 100644
--- a/information_theory/source_coding_fl_direct.v
+++ b/information_theory/source_coding_fl_direct.v
@@ -1,6 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg matrix.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 Require Import Reals Lra.
 From mathcomp Require Import Rstruct.
 Require Import ssrZ ssrR Reals_ext ssr_ext ssralg_ext logb natbin fdist.
@@ -24,7 +24,7 @@ Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
 
 Section encoder_and_decoder.
-Variables (A : finType) (P : {fdist A}) (n k : nat).
+Variables (A : finType) (P : R.-fdist A) (n k : nat).
 
 Variable S : {set 'rV[A]_k.+1}.
 
@@ -208,7 +208,7 @@ rewrite inE /=; apply/negPn/negPn.
     rewrite -exp2_0; apply Exp_le_increasing => //.
     apply mulR_ge0; first exact: leR0n.
     apply addR_ge0; first exact: entropy_ge0.
-    apply Rlt_le; exact: lambda2_gt0.
+    by apply Rlt_le; exact: lambda2_gt0.
   + rewrite addRR -{1}(logK Rlt_0_2) -ExpD {1}/log Log_n //.
     by apply/RleP; rewrite Order.POrderTheory.lexx.
 Qed.
diff --git a/information_theory/source_coding_vl_direct.v b/information_theory/source_coding_vl_direct.v
index d00b6d96..5f6371cf 100644
--- a/information_theory/source_coding_vl_direct.v
+++ b/information_theory/source_coding_vl_direct.v
@@ -1,6 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg matrix.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 Require Import Reals Lra.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext.
@@ -67,7 +67,7 @@ End R_lemma.
 Section Length.
 Variable (X : finType) (n' : nat).
 Let n := n'.+1.
-Variable P : {fdist X}.
+Variable P : R.-fdist X.
 Variable epsilon : R.
 Hypothesis eps_pos : 0 < epsilon.
 
diff --git a/information_theory/string_entropy.v b/information_theory/string_entropy.v
index bb57752e..ec5c4877 100644
--- a/information_theory/string_entropy.v
+++ b/information_theory/string_entropy.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require Import Reals.
-From mathcomp Require Import Rstruct.
+From mathcomp Require Import Rstruct classical_sets.
 Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb.
 Require Import fdist entropy convex ln_facts jensen num_occ.
 
diff --git a/information_theory/success_decode_bound.v b/information_theory/success_decode_bound.v
index 92665419..ba135f11 100644
--- a/information_theory/success_decode_bound.v
+++ b/information_theory/success_decode_bound.v
@@ -140,7 +140,7 @@ apply/le_INR/leP/subset_leq_card/setIidPl/setP => tb.
 by rewrite in_set in_set andbC andbA andbb.
 Qed.
 
-Let partition_pre_image : {set set_of_finType [finType of n.-tuple B]} :=
+Let partition_pre_image (*: {set set_of_finType [finType of n.-tuple B]}*) :=
   [set T_{ `tO( V ) } :&: (@tuple_of_row B n @: (dec tc @^-1: [set Some m])) |
    m in M & [exists y, y \in T_{`tO( V )} :&: (@tuple_of_row B n @: (dec tc @^-1: [set Some m]))]].
 
diff --git a/probability/convex.v b/probability/convex.v
index 9a682386..6971b703 100644
--- a/probability/convex.v
+++ b/probability/convex.v
@@ -2866,12 +2866,12 @@ rewrite mulrDl.
   apply ltR_add; rewrite ltR_pmul2l //; [exact/RltP/prob_gt0 | exact/RltP/onem_gt0/prob_lt1].
 Qed.
 
-Let uniti : set R := (fun x => 0 < x < 1)%coqR.
+Definition uniti : set R := (fun x => 0 < x < 1)%coqR.
 
 Lemma open_unit_interval_convex : is_convex_set uniti.
 Proof. exact: open_interval_convex. Qed.
 
-#[local] HB.instance Definition _ := isConvexSet.Build R uniti open_unit_interval_convex.
+HB.instance Definition _ := isConvexSet.Build R uniti open_unit_interval_convex.
 
 End convex_set_R.