diff --git a/theories/table.v b/theories/table.v
index 9249d52..e5eba1c 100644
--- a/theories/table.v
+++ b/theories/table.v
@@ -53,8 +53,6 @@ Reserved Notation "-oo" (at level 0).
 
 Local Open Scope order_scope.
 
-Hint Resolve le_trans.
-
 Section ext.
 Variable (T : Type).
 
@@ -81,7 +79,7 @@ Arguments is_finite T /.
 Notation "x %:x" := (Fin x).
 Notation "+oo" := (Infty false).
 Notation "-oo" := (Infty true).
-Hint Resolve Fin_inj Infty_inj.
+Hint Resolve Fin_inj Infty_inj : core.
 
 Canonical ext_eqType (T : eqType) := EqType (ext T) (CanEqMixin ext_encodeK).
 Canonical ext_choiceType (T : choiceType) :=
@@ -91,122 +89,15 @@ Canonical ext_countType (T : countType) :=
 Canonical ext_finType (T : finType) :=
   FinType (ext T) (CanFinMixin ext_encodeK).
 
-Section rindex.
+Section lrindex.
 
 Variables (d : unit) (T : orderType d).
+Implicit Types (s : seq T) (t : T).
 
-Notation ext := (ext T).
-Implicit Types (m t u v : T) (x y z : ext).
+Lemma undup_sorted s : sorted <=%O s -> sorted <=%O (undup s).
+Proof. exact/subseq_sorted/undup_subseq/le_trans. Qed.
 
-Let FinT_inj := @Fin_inj T.
-
-Definition ext_le x y := match x, y with
-  | Infty bl, Infty br => br ==> bl | Fin t, Fin u => t <= u
-  | Infty bl, _ => bl               | _, Infty br => ~~ br
-end.
-
-Definition ext_lt x y := match x, y with
-  | Infty bl, Infty br => bl && ~~ br  | Fin t, Fin u => t < u
-  | Infty bl, _ => bl                  | _ , Infty br => ~~ br
-end.
-
-Lemma ext_lt_def : forall x y, ext_lt x y = (y != x) && ext_le x y.
-Proof. by move=> [[]|t] [[]|u]//=; rewrite inj_eq ?lt_def => // ? ? []. Qed.
-
-Lemma ext_le_anti : antisymmetric ext_le.
-Proof. by move=> [[]|t] [[]|u]//= /le_anti->. Qed.
-
-Lemma ext_le_trans : transitive ext_le.
-Proof. by move=> [[]|t] [[]|u] [[]|v]//=; apply: le_trans. Qed.
-
-Lemma ext_le_total : total ext_le.
-Proof. by move=> [[]|t] [[]|u]//=; apply: le_total. Qed.
-
-Definition ext_orderMixin :=
-  LeOrderMixin ext_lt_def (fun _ _ => erefl) (fun _ _ =>  erefl)
-    ext_le_anti ext_le_trans ext_le_total.
-
-Canonical ext_porderType := POrderType d ext ext_orderMixin.
-Canonical ext_latticeType := LatticeType ext ext_orderMixin.
-Canonical ext_dlatticeType := DistrLatticeType ext ext_orderMixin.
-Canonical ext_orderType := OrderType ext ext_orderMixin.
-
-Lemma leEext x y : (x <= y) = (ext_le x y). Proof. by []. Qed.
-Lemma ltEext x y : (x < y) = (ext_lt x y).  Proof. by []. Qed.
-
-Lemma le_ext t t' : (t%:x <= t'%:x) = (t <= t'). Proof. by []. Qed.
-Lemma lt_ext t t' : (t%:x < t'%:x)  = (t < t').  Proof. by []. Qed.
-
-Lemma ge_xmin x : -oo <= x.     Proof. by case: x => [[]|]. Qed.
-Lemma le_xmax x : x <= +oo.     Proof. by case: x => [[]|]. Qed.
-Lemma gt_xmin x : x -> -oo < x. Proof. by case: x. Qed.
-Lemma lt_xmax x : x -> x < +oo. Proof. by case: x. Qed.
-
-Lemma minxmax x : Order.min x +oo = x.   Proof. by case: x => [[]|]. Qed.
-Lemma minmaxx x : Order.min +oo x = x.   Proof. by case: x => [[]|]. Qed.
-Lemma minxmin x : Order.min x -oo = -oo. Proof. by case: x => [[]|]. Qed.
-Lemma minminx x : Order.min -oo x = -oo. Proof. by case: x => [[]|]. Qed.
-
-Lemma maxxmax x : Order.max x +oo = +oo. Proof. by case: x => [[]|]. Qed.
-Lemma maxmaxx x : Order.max +oo x = +oo. Proof. by case: x => [[]|]. Qed.
-Lemma maxxmin x : Order.max x -oo = x.   Proof. by case: x => [[]|]. Qed.
-Lemma maxminx x : Order.max -oo x = x.   Proof. by case: x => [[]|]. Qed.
-
-Definition edflt t t' x :=
-  match x with Fin t'' => t'' | Infty s => if s then t else t' end.
-Notation edflt1 t := (edflt t t).
-
-Lemma le_edflt2  m t t' x x' : t <= m <= t' ->
-  t < edflt1 m x <= t' -> t <= edflt1 m x' < t' ->
-  (edflt t t' x <= edflt t t' x') = (x <= x').
-Proof.
-case: x x' => [[]|u] [[]|v]//= /andP[tm mt] /andP[tu ut] /andP[tv vt];
-do ?by [rewrite ?lexx ?tv ?vt// (le_trans tm)|rewrite ?lt_geF ?(lt_le_trans tu)].
-Qed.
-
-Lemma lt_edflt2  m t t' x x' : t <= m <= t' ->
-  t < edflt1 m x < t' -> t < edflt1 m x' < t' ->
-  (edflt t t' x < edflt t t' x') = (x < x').
-Proof.
-case: x x' => [[]|u] [[]|v]//= /andP[tm mt] /andP[tu ut] /andP[tv vt];
-do ?by [rewrite ?tv ?vt// (lt_trans tu)|rewrite lt_gtF// ?(lt_trans tu)].
-Qed.
-
-Lemma edflt_le_sup m t t' x : t <= m < t' ->
-  edflt1 m x <= t' -> edflt t t' x <= t'.
-Proof. by case: x => [[]|u]//= /andP[tm mt]; apply: le_trans. Qed.
-
-Lemma edflt_ge_inf m t t' x : t < m <= t' ->
-  t <= edflt1 m x -> t <= edflt t t' x.
-Proof. by case: x => [[]|u]//= /andP[tm mt] /le_trans->. Qed.
-
-Lemma ge_edflt t t' t'' x :
-  t <= t'' < t' -> (edflt t t' x <= t'') = (x <= t''%:x).
-Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?tu// lt_geF. Qed.
-
-Lemma le_edflt t t' t'' x :
-  t < t'' <= t' -> (t'' <= edflt t t' x) = (t''%:x <= x).
-Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?ut// lt_geF. Qed.
-
-Lemma gt_edflt t t' t'' x :
-  t < t'' < t' -> (edflt t t' x < t'') = (x < t''%:x).
-Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?tu// lt_gtF//=. Qed.
-
-Lemma lt_edflt t t' t'' x :
-  t < t'' < t' -> (t'' < edflt t t' x) = (t''%:x < x).
-Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?ut// lt_gtF. Qed.
-
-Lemma undup_subseq (s : seq T) : subseq (undup s) s.
-Proof.
-elim: s => //= x s ihs; case: ifP => _; rewrite ?eqxx//.
-case: (undup s) ihs => //= y u yus; case: ifP => // _.
-by rewrite -(subseq_cons2 y) (@subseq_trans _ s)// subseq_cons.
-Qed.
-
-Lemma undup_sorted (s : seq T) : sorted <=%O s -> sorted <=%O (undup s).
-Proof. exact: (subseq_sorted le_trans (undup_subseq s)). Qed.
-
-Lemma all_find (s : seq T) : find predT s = 0. Proof. by elim: s. Qed.
+Lemma all_find s : find predT s = 0. Proof. by elim: s. Qed.
 
 Section lrindex_def.
 Variable (x0 : T) (s : seq T).
@@ -218,14 +109,12 @@ Notation rindex t := (find (> t) s).
 
 Lemma eq_count_undup : s = flatten [seq nseq (count_mem x s) x | x <- undup s].
 Proof.
-rewrite (eq_sorted le_trans le_anti _ _ ((@perm_count_undup _ _)))//.
+rewrite (le_sorted_eq _ _ (@perm_count_undup _ _)) //.
 have := subseq_sorted le_trans (undup_subseq s) s_sorted.
 elim: (undup) => //= x l ihl; rewrite path_sortedE// => /andP[/allP le_xl l_s].
 elim: (count_mem _ _)=> [|/= k ihk]; rewrite ?path_min_sorted ?ihl//.
-apply/allP => y; rewrite mem_cat mem_nseq.
-case: eqP => [->//|_]; rewrite andbF/=.
-move=> /flattenP[z /mapP[w wl ->]]; rewrite mem_nseq => /andP[_ /eqP ->].
-by apply: le_xl.
+rewrite all_cat all_nseq lexx orbT; apply/allP=> y /flattenP [z /mapP[w wl ->]].
+by rewrite mem_nseq => /andP [_ /eqP ->]; apply: le_xl.
 Qed.
 
 Lemma lindex_size t : (lindex t <= size s)%N. Proof. exact: find_size. Qed.
@@ -236,8 +125,7 @@ Proof. by rewrite sub_find => // u /ltW. Qed.
 
 Lemma eq_lrindex t : t \notin s -> lindex t = rindex t.
 Proof.
-move=> tNs; apply: eq_in_find.
-by move=> t' t's; rewrite lt_neqAle; case: eqP t's tNs => //-> ->.
+by move=> tNs; apply: eq_in_find => t' t's; case: ltgtP t's tNs => // -> ->.
 Qed.
 
 (* ---- t -- i ----- j ---- *)
@@ -245,7 +133,7 @@ Lemma lindex_le t j : (j < size s)%N -> (lindex t <= j)%N = (t <= nth x0 s j)%O.
 Proof.
 move=> j_lt; set i := find _ _.
 case: (leqP i) => [ij|/(before_find x0)//]; have i_lt := leq_ltn_trans ij j_lt.
-rewrite (@le_trans _ _ (nth x0 s i)) ?sorted_le_nth ?nth_find ?has_find//.
+rewrite (@le_trans _ _ (nth x0 s i)) ?sorted_leq_nth ?nth_find ?has_find//.
 Qed.
 
 Lemma lindex_gt t j : (j < size s)%N -> (j < lindex t)%N = (nth x0 s j < t)%O.
@@ -263,7 +151,7 @@ Lemma rindex_le t j : (j < size s)%N -> (rindex t <= j)%N = (t < nth x0 s j)%O.
 Proof.
 move=> j_lt; set i := find _ _.
 case: (leqP i) => [ij|/(before_find x0)//]; have i_lt := leq_ltn_trans ij j_lt.
-by rewrite (@lt_le_trans _ _ (nth x0 s i)) ?sorted_le_nth ?nth_find ?has_find.
+by rewrite (@lt_le_trans _ _ (nth x0 s i)) ?sorted_leq_nth ?nth_find ?has_find.
 Qed.
 
 Lemma rindex_gt t j : (j < size s)%N -> (j < rindex t)%N = (nth x0 s j <= t)%O.
@@ -283,19 +171,18 @@ Proof. by move=> t_in; rewrite -has_find; apply/hasP; exists t. Qed.
 Lemma rindex_gt0 t : t \in s -> (rindex t > 0)%N.
 Proof.
 move=> /(nthP x0)[i i_lt <- {t}]; have s_gt0 := leq_trans (ltn0Sn i) i_lt.
-by rewrite rindex_gt// sorted_le_nth.
+by rewrite rindex_gt// sorted_leq_nth.
 Qed.
 
 Lemma lindex_in t : t \in s -> lindex t = index t s.
 Proof.
-move=> ts; elim: s ts s_sorted => //= x l ihl; rewrite inE => /predU1P[<-|tl].
-  by rewrite lexx eqxx.
-rewrite path_sortedE // => /andP[/allP le_xl l_sorted].
-by rewrite le_eqVlt eq_sym le_gtF ?le_xl// orbF ihl.
+move=> ts; elim: s ts s_sorted => //= x l ihl; rewrite inE path_sortedE //.
+case: ltgtP => [|xt tl /andP [_] /ihl ->|] //.
+by move=> tx tl /andP [/allP /(_ _ tl)]; rewrite leNgt tx.
 Qed.
 
 End lrindex_def.
-Hint Resolve lindex_size rindex_size le_lrindex.
+Hint Resolve lindex_size rindex_size le_lrindex : core.
 Notation lindex s t := (find (>= t) s).
 Notation rindex s t := (find (> t) s).
 
@@ -335,7 +222,7 @@ End lrindex_theory.
 
 Section lrindex_take_drop.
 
-Lemma take_lindex s t : sorted <=%O%O s ->
+Lemma take_lindex s t : sorted <=%O s ->
   take (lindex s t) s = [seq y <- s | (y < t)%O].
 Proof.
 elim: s => //= a s IHs pas; rewrite -IHs ?(path_sorted pas)//.
@@ -343,7 +230,7 @@ case: leP => //= le_ta; rewrite le_lindex ?take0//.
 by have /(order_path_min le_trans) := pas; apply/sub_all => y; apply: le_trans.
 Qed.
 
-Lemma drop_lindex s t : sorted <=%O%O s ->
+Lemma drop_lindex s t : sorted <=%O s ->
   drop (lindex s t) s = [seq y <- s | (y >= t)%O].
 Proof.
 elim: s => //= a s IHs pas; rewrite -IHs ?(path_sorted pas)//.
@@ -351,7 +238,7 @@ case: leP => //= le_ta; rewrite le_lindex ?drop0//.
 by have /(order_path_min le_trans) := pas; apply/sub_all => y; apply: le_trans.
 Qed.
 
-Lemma take_rindex s t : sorted <=%O%O s ->
+Lemma take_rindex s t : sorted <=%O s ->
   take (rindex s t) s = [seq y <- s | (y <= t)%O].
 Proof.
 elim: s => //= a s IHs pas; rewrite -IHs ?(path_sorted pas)//.
@@ -360,7 +247,7 @@ have /(order_path_min le_trans) := pas; apply/sub_all => y.
 exact: lt_le_trans.
 Qed.
 
-Lemma drop_rindex s t : sorted <=%O%O s ->
+Lemma drop_rindex s t : sorted <=%O s ->
   drop (rindex s t) s = [seq y <- s | (y > t)%O].
 Proof.
 elim: s => //= a s IHs pas; rewrite -IHs ?(path_sorted pas)//.
@@ -373,21 +260,16 @@ Variable (s : seq T).
 Hypothesis s_sorted : sorted <=%O s.
 
 Lemma lindex_count t : lindex s t = count (< t) s.
-Proof.
-by rewrite -size_filter -take_lindex ?size_take; case: ltngtP (lindex_size s t).
-Qed.
+Proof. by rewrite -size_filter -take_lindex ?size_takel. Qed.
 
 Lemma rindex_count t : rindex s t = count (<= t) s.
-Proof.
-by rewrite -size_filter -take_rindex ?size_take; case: ltngtP (rindex_size s t).
-Qed.
+Proof. by rewrite -size_filter -take_rindex ?size_takel. Qed.
 
 Lemma rindexEl t : rindex s t = count_mem t s + lindex s t.
 Proof.
 rewrite rindex_count// lindex_count// -count_predUI.
-rewrite (@eq_count _ (predU _ _) (<= t)); last by move=> y /=; case: ltgtP.
 rewrite (@eq_count _ (predI _ _) pred0); last by move=> y /=; case: ltgtP.
-by rewrite count_pred0 addn0.
+by rewrite count_pred0 addn0; apply: eq_count => x /=; case: ltgtP.
 Qed.
 
 Lemma leqif_lrindex t : lindex s t <= rindex s t ?= iff (t \notin s).
@@ -406,6 +288,117 @@ Proof. by move=> ts; rewrite rindex_uniq ts lindex_in. Qed.
 
 End lrindex_take_drop.
 
+End lrindex.
+Global Hint Resolve lindex_size rindex_size le_lrindex : core.
+
+Notation lindex s t := (find (>= t) s).
+Notation rindex s t := (find (> t) s).
+
+Section ext_theory.
+
+Variables (d : unit) (T : orderType d).
+
+Notation ext := (ext T).
+Implicit Types (m t u v : T) (x y z : ext).
+
+Let FinT_inj := @Fin_inj T.
+
+Definition ext_le x y := match x, y with
+  | Infty bl, Infty br => br ==> bl | Fin t, Fin u => t <= u
+  | Infty bl, _ => bl               | _, Infty br => ~~ br
+end.
+
+Definition ext_lt x y := match x, y with
+  | Infty bl, Infty br => bl && ~~ br  | Fin t, Fin u => t < u
+  | Infty bl, _ => bl                  | _ , Infty br => ~~ br
+end.
+
+Lemma ext_lt_def : forall x y, ext_lt x y = (y != x) && ext_le x y.
+Proof. by move=> [[]|t] [[]|u]//=; rewrite inj_eq ?lt_def => // ? ? []. Qed.
+
+Lemma ext_le_anti : antisymmetric ext_le.
+Proof. by move=> [[]|t] [[]|u]//= /le_anti->. Qed.
+
+Lemma ext_le_trans : transitive ext_le.
+Proof. by move=> [[]|t] [[]|u] [[]|v]//=; apply: le_trans. Qed.
+
+Lemma ext_le_total : total ext_le.
+Proof. by move=> [[]|t] [[]|u]//=; apply: le_total. Qed.
+
+Definition ext_orderMixin :=
+  LeOrderMixin ext_lt_def (fun _ _ => erefl) (fun _ _ =>  erefl)
+    ext_le_anti ext_le_trans ext_le_total.
+
+Canonical ext_porderType := POrderType d ext ext_orderMixin.
+Canonical ext_latticeType := LatticeType ext ext_orderMixin.
+Canonical ext_dlatticeType := DistrLatticeType ext ext_orderMixin.
+Canonical ext_orderType := OrderType ext ext_orderMixin.
+
+Lemma leEext x y : (x <= y) = (ext_le x y). Proof. by []. Qed.
+Lemma ltEext x y : (x < y) = (ext_lt x y).  Proof. by []. Qed.
+
+Lemma le_ext t t' : (t%:x <= t'%:x) = (t <= t'). Proof. by []. Qed.
+Lemma lt_ext t t' : (t%:x < t'%:x)  = (t < t').  Proof. by []. Qed.
+
+Lemma ge_xmin x : -oo <= x.     Proof. by case: x => [[]|]. Qed.
+Lemma le_xmax x : x <= +oo.     Proof. by case: x => [[]|]. Qed.
+Lemma gt_xmin x : x -> -oo < x. Proof. by case: x. Qed.
+Lemma lt_xmax x : x -> x < +oo. Proof. by case: x. Qed.
+
+Lemma minxmax x : Order.min x +oo = x.   Proof. by case: x => [[]|]. Qed.
+Lemma minmaxx x : Order.min +oo x = x.   Proof. by case: x => [[]|]. Qed.
+Lemma minxmin x : Order.min x -oo = -oo. Proof. by case: x => [[]|]. Qed.
+Lemma minminx x : Order.min -oo x = -oo. Proof. by case: x => [[]|]. Qed.
+
+Lemma maxxmax x : Order.max x +oo = +oo. Proof. by case: x => [[]|]. Qed.
+Lemma maxmaxx x : Order.max +oo x = +oo. Proof. by case: x => [[]|]. Qed.
+Lemma maxxmin x : Order.max x -oo = x.   Proof. by case: x => [[]|]. Qed.
+Lemma maxminx x : Order.max -oo x = x.   Proof. by case: x => [[]|]. Qed.
+
+Definition edflt t t' x :=
+  match x with Fin t'' => t'' | Infty s => if s then t else t' end.
+Notation edflt1 t := (edflt t t).
+
+Lemma le_edflt2  m t t' x x' : t <= m <= t' ->
+  t < edflt1 m x <= t' -> t <= edflt1 m x' < t' ->
+  (edflt t t' x <= edflt t t' x') = (x <= x').
+Proof.
+case: x x' => [[]|u] [[]|v]//= /andP[tm mt] /andP[tu ut] /andP[tv vt];
+do ?by [rewrite ?lexx ?tv ?vt// (le_trans tm)|rewrite ?lt_geF ?(lt_le_trans tu)].
+Qed.
+
+Lemma lt_edflt2  m t t' x x' : t <= m <= t' ->
+  t < edflt1 m x < t' -> t < edflt1 m x' < t' ->
+  (edflt t t' x < edflt t t' x') = (x < x').
+Proof.
+case: x x' => [[]|u] [[]|v]//= /andP[tm mt] /andP[tu ut] /andP[tv vt];
+do ?by [rewrite ?tv ?vt// (lt_trans tu)|rewrite lt_gtF// ?(lt_trans tu)].
+Qed.
+
+Lemma edflt_le_sup m t t' x : t <= m < t' ->
+  edflt1 m x <= t' -> edflt t t' x <= t'.
+Proof. by case: x => [[]|u]//= /andP[tm mt]; apply: le_trans. Qed.
+
+Lemma edflt_ge_inf m t t' x : t < m <= t' ->
+  t <= edflt1 m x -> t <= edflt t t' x.
+Proof. by case: x => [[]|u]//= /andP[tm mt] /le_trans->. Qed.
+
+Lemma ge_edflt t t' t'' x :
+  t <= t'' < t' -> (edflt t t' x <= t'') = (x <= t''%:x).
+Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?tu// lt_geF. Qed.
+
+Lemma le_edflt t t' t'' x :
+  t < t'' <= t' -> (t'' <= edflt t t' x) = (t''%:x <= x).
+Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?ut// lt_geF. Qed.
+
+Lemma gt_edflt t t' t'' x :
+  t < t'' < t' -> (edflt t t' x < t'') = (x < t''%:x).
+Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?tu// lt_gtF//=. Qed.
+
+Lemma lt_edflt t t' t'' x :
+  t < t'' < t' -> (t'' < edflt t t' x) = (t''%:x < x).
+Proof. by case: x => [[]|u]//= /andP[tu ut]; rewrite ?ut// lt_gtF. Qed.
+
 Section ext_seq.
 
 Variable (s : seq T).
@@ -436,17 +429,16 @@ Proof. by rewrite subseq_cons2 -cats1 prefix_subseq. Qed.
 
 Lemma ext_seqrl_sorted : sorted <=%O ext_seqrl.
 Proof.
-rewrite /= path_min_sorted ?sorted_map//; last first.
-  by apply/allP => x; rewrite ge_xmin.
+rewrite /= path_min_sorted; last by apply/allP => x; rewrite ge_xmin.
 rewrite -(rev_sorted >=%O) rev_rcons/= path_min_sorted; last first.
   by apply/allP => x /=; rewrite le_xmax.
 by rewrite rev_sorted ?sorted_map.
 Qed.
-Hint Resolve ext_seqrl_sorted.
+Hint Resolve ext_seqrl_sorted : core.
 
 Definition ext_seq_sorted :=
   subseq_sorted le_trans subseq_extrl ext_seqrl_sorted.
-Hint Resolve ext_seq_sorted.
+Hint Resolve ext_seq_sorted : core.
 
 Lemma eq_from_lindex i j x : [i] < x <= [i.+1] -> [j] < x <= [j.+1] -> i = j.
 Proof.
@@ -454,8 +446,8 @@ wlog lt_ij : i j / (i < j)%N => [hw ti tj|/andP[it ti] /andP[jt tj]].
   by have [/hw->//|/hw->//|//] := ltngtP i j.
 have [i_le|i_ge] := leqP j (size s); last first.
   by have := lt_le_trans jt tj; rewrite nth_default/= ?size_map// ltNge le_xmax.
-suff /(le_trans ti) /le_lt_trans /(_ jt) : [i.+1] <= [j] by rewrite ltxx.
-by rewrite sorted_le_nth -?topredE//= ?size_map// ?ltnS (leq_trans lt_ij).
+suff: [i.+1] <= [j] by rewrite leNgt (lt_le_trans jt).
+by rewrite sorted_leq_nth -?topredE//= ?size_map // ltnS (leq_trans lt_ij).
 Qed.
 
 Lemma eq_from_rindex i j x : [i] <= x < [i.+1] -> [j] <= x < [j.+1] -> i = j.
@@ -464,39 +456,38 @@ wlog lt_ij : i j / (i < j)%N => [hw ti tj|/andP[it ti] /andP[jt tj]].
   by have [/hw->//|/hw->//|//] := ltngtP i j.
 have [i_le|i_ge] := leqP j (size s); last first.
   by have := le_lt_trans jt tj; rewrite nth_default/= ?size_map// ltNge le_xmax.
-suff /(lt_le_trans ti) /lt_le_trans/(_ jt) : [i.+1] <= [j] by rewrite ltxx.
-by rewrite sorted_le_nth -?topredE//= ?size_map// ?ltnS (leq_trans lt_ij).
+suff: [i.+1] <= [j] by rewrite leNgt (le_lt_trans jt).
+by rewrite sorted_leq_nth -?topredE//= ?size_map// ltnS (leq_trans lt_ij).
 Qed.
 
 Hypothesis s_uniq : uniq s.
 
 Let s_lt_sorted : sorted <%O s.
 Proof. by rewrite lt_sorted_uniq_le s_uniq. Qed.
-Hint Resolve le_trans lt_trans.
 
 Lemma ext_seqrl_uniq : uniq ext_seqrl.
 Proof.
 rewrite /= ?rcons_uniq ?mem_rcons map_inj_uniq ?s_uniq ?andbT//=.
 by apply/andP; split; apply/negP=> /mapP[].
 Qed.
-Hint Resolve ext_seqrl_uniq.
+Hint Resolve ext_seqrl_uniq : core.
 
 Definition ext_seq_uniq := subseq_uniq subseq_extrl ext_seqrl_uniq.
-Hint Resolve ext_seq_uniq.
+Hint Resolve ext_seq_uniq : core.
 
 Lemma ext_seqrl_lt_sorted : sorted <%O ext_seqrl.
 Proof. by rewrite lt_sorted_uniq_le ext_seqrl_uniq. Qed.
-Hint Resolve ext_seqrl_lt_sorted.
+Hint Resolve ext_seqrl_lt_sorted : core.
 
 Definition ext_seq_lt_sorted :=
   subseq_sorted lt_trans subseq_extrl ext_seqrl_lt_sorted.
-Hint Resolve ext_seq_lt_sorted.
+Hint Resolve ext_seq_lt_sorted : core.
 
 Lemma le_nth_ext : {in [pred i | (i <= (size s).+1)%N] &,
   {mono nth +oo ext_seq : i j / (i <= j)%N >-> i <= j}}.
 Proof.
 apply: le_mono_in => i j i_s j_s; rewrite !nth_extrl.
-by apply: (sorted_lt_nth lt_trans _ _); rewrite // inE/= size_rcons size_map.
+by apply: (sorted_ltn_nth lt_trans); rewrite // inE/= size_rcons size_map.
 Qed.
 
 Lemma lt_nth_ext : {in [pred i | (i <= (size s).+1)%N] &,
@@ -522,15 +513,10 @@ Lemma eq_in_aprev t : t \in s -> t%:x = aprev t.
 Proof. by rewrite aprevE; case: ifP. Qed.
 
 Lemma in_sprev t : sprev t \in -oo :: map Fin s.
-Proof.
-rewrite /sprev /= in_cons; case: (lindex _ _) (lindex_size s t) => //= n n_lt.
-by rewrite (nth_map t)// mem_map// mem_nth.
-Qed.
+Proof. by apply: mem_nth; rewrite /= ltnS size_map lindex_size. Qed.
 
 Lemma in_aprev t : aprev t \in -oo :: map Fin s.
-Proof.
-by rewrite aprevE; case: ifPn => [ts|_]; rewrite ?in_sprev// in_cons mem_map.
-Qed.
+Proof. by apply: mem_nth; rewrite /= ltnS size_map rindex_size. Qed.
 
 Lemma in_snext t : snext t \in +oo :: map Fin s.
 Proof.
@@ -541,53 +527,49 @@ Qed.
 
 Lemma in_anext t : anext t \in +oo :: map Fin s.
 Proof.
-by rewrite anextE; case: ifPn => [ts|_]; rewrite ?in_snext// in_cons mem_map.
+rewrite /anext /= in_cons; case: (ltnP (lindex s t) (size (map Fin s))).
+  by move=> /mem_nth ->; rewrite orbT.
+by move=> /(nth_default _)->.
 Qed.
 
 Lemma sprev_snextP t : sprev t < t%:x < snext t.
 Proof.
-rewrite /sprev /snext; have [ts|tNs] := boolP (t \in s).
-  rewrite [X in _ < X]eq_in_anext// [_%:x as X in X < _]eq_in_aprev//.
-  by rewrite !lt_nth_ext ?leqnn ?inE ?ltnS ?leqW.
-rewrite /snext /sprev/=; apply/andP; split; last first.
-  case: (ltngtP (size _)) (rindex_size s t) => [//|i_lt|<-] _; last first.
-    by rewrite nth_default//= ?size_map.
+rewrite /snext -lindex_gt //= ?ltnS ?size_map ?lindex_size // find_map leqnn /=.
+case: (ltngtP (size _)) (rindex_size s t) => [//|i_lt|<-] _.
   by rewrite /= (nth_map t)// ltEext/= nth_find// has_find.
-have /= := @before_find _ t (>= t) s (lindex s t).-1; rewrite -/(lindex s t).
-case: (lindex _ _) (lindex_size s t) => //= i i_lt  /(_ (ltnSn _))/negbT.
-by rewrite (nth_map t)// ltEext/= -ltNge.
+by rewrite nth_default//= ?size_map.
 Qed.
-Hint Resolve sprev_snextP.
+Hint Resolve sprev_snextP : core.
 
 Lemma gt_sprev t : sprev t < t%:x. Proof. by case/andP: (sprev_snextP t). Qed.
-Hint Resolve gt_sprev.
+Hint Resolve gt_sprev : core.
 
 Lemma ge_sprev t : sprev t <= t%:x. Proof. by rewrite ltW. Qed.
-Hint Resolve ge_sprev.
+Hint Resolve ge_sprev : core.
 
 Lemma geif_aprev t : aprev t <= t%:x ?= iff (t \in s).
 Proof.
 by apply/leifP; rewrite aprevE ?(fun_if, if_arg) eqxx gt_sprev; case: ifP => ->.
 Qed.
-Hint Resolve geif_aprev.
+Hint Resolve geif_aprev : core.
 
 Lemma ge_aprev t : aprev t <= t%:x. Proof. by rewrite geif_aprev. Qed.
-Hint Resolve ge_aprev.
+Hint Resolve ge_aprev : core.
 
 Lemma lt_snext t : t%:x < snext t. Proof. by case/andP: (sprev_snextP t). Qed.
-Hint Resolve lt_snext.
+Hint Resolve lt_snext : core.
 
 Lemma le_snext t : t%:x <= snext t. Proof. by rewrite ltW. Qed.
-Hint Resolve le_snext.
+Hint Resolve le_snext : core.
 
 Lemma leif_anext t : t%:x <= anext t ?= iff (t \in s).
 Proof.
 by apply/leifP; rewrite anextE ?(fun_if, if_arg) eqxx lt_snext; case: ifP => ->.
 Qed.
-Hint Resolve leif_anext.
+Hint Resolve leif_anext : core.
 
 Lemma le_anext t : t%:x <= anext t. Proof. by rewrite leif_anext. Qed.
-Hint Resolve le_anext.
+Hint Resolve le_anext : core.
 
 Lemma eq_lindex t u : sprev t < u%:x <= anext t -> lindex s t = lindex s u.
 Proof. by move=> /eq_from_lindex; apply; rewrite ?gt_sprev ?le_anext. Qed.
@@ -597,26 +579,28 @@ Proof. by move=> /eq_from_rindex; apply; rewrite ?ge_aprev ?lt_snext. Qed.
 
 Lemma lt_sprev_anext t : sprev t < anext t.
 Proof. by have := lt_le_trans (gt_sprev t) (le_anext t). Qed.
-Hint Resolve lt_sprev_anext.
+Hint Resolve lt_sprev_anext : core.
 
 Lemma lt_aprev_snext t : aprev t < snext t.
 Proof. by have := le_lt_trans (ge_aprev t) (lt_snext t). Qed.
-Hint Resolve lt_aprev_snext.
+Hint Resolve lt_aprev_snext : core.
 
 Lemma lt_sprev_snext t : sprev t < snext t.
 Proof. by have := lt_trans (gt_sprev t) (lt_snext t). Qed.
-Hint Resolve lt_sprev_snext.
+Hint Resolve lt_sprev_snext : core.
 
 Section sorted_mono.
 Variables (d' : unit) (T' : orderType d) (t0 : T')
   (s' : seq T') (ss : sorted <%O s') (ssle : sorted <=%O s').
-Definition total_sorted_le_nthW := sorted_le_nth (@le_trans _ _) (@lexx _ _) t0 ssle.
-Let sorted_lt_nthW := sorted_lt_nth (@lt_trans _ _) t0 ss.
-Definition total_sorted_le_nth := le_mono_in sorted_lt_nthW.
-Definition total_sorted_lt_nth := leW_mono_in total_sorted_le_nth.
+Definition total_sorted_leq_nthW :=
+  sorted_leq_nth (@le_trans _ _) (@lexx _ _) t0 ssle.
+Let sorted_ltn_nthW := sorted_ltn_nth (@lt_trans _ _) t0 ss.
+Definition total_sorted_leq_nth := le_mono_in sorted_ltn_nthW.
+Definition total_sorted_ltn_nth := leW_mono_in total_sorted_leq_nth.
 End sorted_mono.
 
-Lemma lindex_eq i : {in [pred t | [i] < t%:x <= [i.+1]], forall t, lindex s t = i}.
+Lemma lindex_eq i :
+  {in [pred t | [i] < t%:x <= [i.+1]], forall t, lindex s t = i}.
 Proof. by move=> t; apply: eq_from_lindex; rewrite gt_sprev le_anext. Qed.
 
 Lemma lindex_eql u : {in [pred t | sprev u < t%:x <= u%:x],
@@ -626,30 +610,35 @@ move=> t; rewrite inE => /andP[ut tu].
 by rewrite (@lindex_eq (lindex s u))// inE ut (le_trans tu)// le_anext.
 Qed.
 
-Lemma rindex_eq i : {in [pred t | [i] <= t%:x < [i.+1]], forall t, rindex s t = i}.
+Lemma rindex_eq i :
+  {in [pred t | [i] <= t%:x < [i.+1]], forall t, rindex s t = i}.
 Proof. by move=> t; apply: eq_from_rindex; rewrite ge_aprev lt_snext. Qed.
 
-Lemma ext_inF i : {in [pred t | [i] < t%:x < [i.+1]], forall t, t \in s = false}.
+Lemma ext_inF i :
+  {in [pred t | [i] < t%:x < [i.+1]], forall t, t \in s = false}.
 Proof.
-move=> t; rewrite inE => /andP[t_gt t_lt]; have := t_lt.
-(* rewrite -(@lindexE i t); last by rewrite inE t_gt ltW. *)
-(* by apply: contraTF => /mem_rnext->; rewrite ltxx. *)
-Admitted.
+move=> t /andP []; case: (ltngtP i (size s)) => [lt_is|lt_si|->].
+- rewrite -lindex_gt -?rindex_le //= ?ltnS ?size_map ?(ltnW lt_is) //.
+  move=> + ge_i; apply: contra_leqF => ts; move: ge_i.
+  by rewrite lindex_in ?rindex_in ?sorted_map ?mem_map ?map_inj_uniq.
+- by rewrite nth_default //= size_map.
+- move=> + _; apply: contra_ltF => ts.
+  rewrite -lindex_le //= ?ltnS ?size_map //.
+  by rewrite -(size_map Fin) -has_find has_map; apply/hasP; exists t => /=.
+Qed.
 
 Lemma lrindex_notin i :
   {in [pred t | [i] < t%:x < [i.+1]], forall t, t \notin s}.
-Proof. (* by move=> x /lindex_inF->. Qed. *) Admitted.
+Proof. by move=> x /ext_inF ->. Qed.
 
 Lemma lindex_next t tnext : anext t = tnext%:x -> lindex s tnext = lindex s t.
 (* Proof. by move=> sneq; apply: lindexE; rewrite inE -sneq lexx andbT. Qed. *)
 Admitted.
 
 End ext_seq.
-End rindex.
+End ext_theory.
 
 Bind Scope ext_scope with ext.
 Notation edflt1 t := (edflt t t).
 Notation "s `[ i ]" := (nth +oo%x (ext_seq s) i) : ext_scope.
-Notation lindex s t := (find (>= t) s).
-Notation rindex s t := (find (> t) s).
 (* Hint Resolve lrindex_size lrindexP gt_rprev ge_rprev le_rnext lt_rprev_rnext. *)