diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 052158a..47f2c2a 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,16 +17,15 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v2
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-mathcomp-trajectories.opam'
           custom_image: ${{ matrix.image }}
 
-
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/README.md b/README.md
index a870c3e..33f48d4 100644
--- a/README.md
+++ b/README.md
@@ -6,23 +6,13 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/math-comp/trajectories/actions/workflows/docker-action.yml/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/trajectories/actions/workflows/docker-action.yml
+[docker-action-shield]: https://github.com/math-comp/trajectories/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/trajectories/actions?query=workflow:"Docker%20CI"
 
-This directory contain a variety of developments that were  thought to be
-useful for the computation of trajectories between obstacles.
 
-The leading example relies on a decomposition of a plane area in vertical
-cells, which gives a graph whose nodes are the cells.  The next step is to
-compute a path in this graph, from which a piecewise straight line
-trajectory is computed, which is guaranted to stay inside the safe cells, or
-to go from one cell to a neighbor only through a safe crossing.  The final
-step is to smoothen the trajectory, by using Bezier curves for which checks
-are performed to verify that they stay within the safe part of the area.
 
-A demonstration version is available at 
-[this page](https://stamp.gitlabpages.inria.fr/trajectories.html).
 
+TODO
 
 ## Meta
 
@@ -30,7 +20,7 @@ A demonstration version is available at
   - Reynald Affeldt (initial)
   - Yves Bertot (initial)
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq >= 8.17, MathComp >= 2.2.0
+- Compatible Coq versions: Coq >= 8.19, MathComp >= 2.2.0
 - Additional dependencies:
   - [MathComp ssreflect 2.2.0 or later](https://math-comp.github.io)
   - [MathComp fingroup 2.2.0 or later](https://math-comp.github.io)
@@ -39,8 +29,8 @@ A demonstration version is available at
   - [MathComp field 2.2.0 or later](https://math-comp.github.io)
   - [Mathcomp real closed 2.0.0 or later](https://github.com/math-comp/real-closed/)
   - [Algebra tactics 1.2.0 or later](https://github.com/math-comp/algebra-tactics)
-  - [MathComp analysis 1.0.0 or later](https://github.com/math-comp/analysis)
-  - [Infotheo 0.7.0 of later](https://github.com/affeldt-aist/infotheo)
+  - [MathComp analysis 1.9.0 or later](https://github.com/math-comp/analysis)
+  - [Infotheo 0.9.1 of later](https://github.com/affeldt-aist/infotheo)
 - Coq namespace: `mathcomp.trajectories`
 - Related publication(s):
   - [Safe Smooth Paths between Straight Line Obstacles](https://inria.hal.science/hal-04312815) doi:[https://doi.org/10.1007/978-3-031-61716-4_3](https://doi.org/https://doi.org/10.1007/978-3-031-61716-4_3)
diff --git a/_CoqProject b/_CoqProject
index 705382a..711b00d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -9,7 +9,6 @@ theories/civt.v
 theories/desc.v
 theories/desc1.v
 theories/desc2.v
-theories/infra.v
 theories/bern.v
 theories/bern5.v
 theories/casteljau.v
diff --git a/coq-mathcomp-trajectories.opam b/coq-mathcomp-trajectories.opam
index db76215..6e4f838 100644
--- a/coq-mathcomp-trajectories.opam
+++ b/coq-mathcomp-trajectories.opam
@@ -14,10 +14,10 @@ synopsis: "Trajectories"
 description: """
 TODO"""
 
-build: [make "-j%{jobs}%"]
+build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.17" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") }
@@ -25,8 +25,8 @@ depends: [
   "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-real-closed" { (>= "2.0.0") | (= "dev") }
   "coq-mathcomp-algebra-tactics" { (>= "1.2.0") | (= "dev") }
-  "coq-mathcomp-analysis" { (>= "1.0.0") }
-  "coq-infotheo" { >= "0.7.0"}
+  "coq-mathcomp-analysis" { (>= "1.9.0") }
+  "coq-infotheo" { >= "0.9.1"}
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index 60a7716..a270f37 100644
--- a/meta.yml
+++ b/meta.yml
@@ -27,11 +27,11 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq >= 8.17, MathComp >= 2.2.0
-  opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }'
+  text: Coq >= 8.19, MathComp >= 2.2.0
+  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.19'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
@@ -72,14 +72,14 @@ dependencies:
     [Algebra tactics 1.2.0 or later](https://github.com/math-comp/algebra-tactics)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.0.0") }'
+    version: '{ (>= "1.9.0") }'
   description: |-
-    [MathComp analysis 1.0.0 or later](https://github.com/math-comp/analysis)
+    [MathComp analysis 1.9.0 or later](https://github.com/math-comp/analysis)
 - opam:
     name: coq-infotheo
-    version: '{ >= "0.7.0"}'
+    version: '{ >= "0.9.1"}'
   description: |-
-    [Infotheo 0.7.0 of later](https://github.com/affeldt-aist/infotheo)
+    [Infotheo 0.9.1 of later](https://github.com/affeldt-aist/infotheo)
 
 namespace: mathcomp.trajectories
 
diff --git a/theories/cells_alg.v b/theories/cells_alg.v
index b0ca9ee..49ca808 100644
--- a/theories/cells_alg.v
+++ b/theories/cells_alg.v
@@ -4959,7 +4959,7 @@ Record common_invariant bottom top edge_set s
      lexePt (point (head dummy_event events)) (right_pt g)}
 }.
 
-Record common_non_gp_invariant bottom top edge_set s 
+Record common_non_gp_invariant bottom top edge_set s
   (all_events processed_events events : seq event) :=
   { ngcomm : common_invariant bottom top edge_set s all_events
     processed_events events;
diff --git a/theories/convex.v b/theories/convex.v
index e9af65b..c4370a7 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -1,14 +1,14 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra vector mathcomp_extra.
-From mathcomp Require Import reals ereal classical_sets boolp Rstruct lra.
-From infotheo Require Import ssrR Reals_ext realType_ext fdist convex.
+From mathcomp Require Import all_ssreflect all_algebra lra.
+From mathcomp Require Import mathcomp_extra boolp Rstruct classical_sets.
+From mathcomp Require Import reals ereal interval_inference.
+From infotheo Require Import realType_ext fdist convex.
 Require Import preliminaries.
 
 Import Order.POrderTheory Order.TotalTheory GRing.Theory Num.Theory preliminaries.
 Import fdist convex.
 Local Open Scope ring_scope.
 
-Require Import Reals.
 Local Close Scope N_scope.
 Delimit Scope nat_scope with N.
 Delimit Scope int_scope with Z.
@@ -18,8 +18,10 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Local Definition R := Rdefinitions.R.
+
 Section convex.
-Variable (E : convType).
+Variable (E : convType R).
 
 Local Open Scope classical_set_scope.
 Local Open Scope convex_scope.
@@ -35,7 +37,8 @@ apply/asboolP =>x y p [Cx Dx] [Cy Dy]; split.
 by move/asboolP: (convex_setP D); apply.
 Qed.
 
-Lemma hullX (F : convType) (C : set E) (D : set F) : hull (C `*` D) = hull C `*` hull D.
+Lemma hullX (F : @convType R) (C : set E) (D : set F) :
+  hull (C `*` D) = hull C `*` hull D.
 Proof.
 rewrite eqEsubset; split.
    move=>+ [n][/=g][/=d][gCD]-> =>_.
@@ -47,43 +50,39 @@ move=>[+ +][]/=[n][g][d][gC->][m][f][e] [fD->]=>_ _.
 exists (n * m)%N, (fun i=> let (i, j) := split_prod i in (g i, f j)), (fdistmap (unsplit_prod (n:=m)) (d `x e)%fdist); split.
    move=>+ [i] _ <- =>_.
    by case: (split_prod i)=>a b; split; [apply gC | apply fD].
-rewrite Convn_pair/comp/=; congr pair; apply S1_inj; rewrite !S1_Convn big_prod_ord/=.
+rewrite Convn_pair/comp/=; congr pair;
+    apply: (S1_inj R); rewrite [LHS]S1_Convn [RHS]S1_Convn big_prod_ord/=.
   apply eq_big => // i _.
-  rewrite -(scale1pt (scalept _ _)) scaleptA // -[(1 * d i)%coqR]/(1 * d i) -(FDist.f1 e).
+  rewrite -(scale1pt (scalept _ _)) scaleptA // -(FDist.f1 e).
   rewrite mulr_suml.
-  have @h : nneg_fun 'I_m.
-    (* BUG HB.pack *)
-    exists (fun j => e j * d i)%coqR => j.
-    by apply: ssrR.mulR_ge0.
+  pose h x := e x * d i.
+  have h0 x : 0 <= h x by rewrite /h mulr_ge0.
   under eq_bigr => j _ do rewrite -[e j * d i]/(h j).
-  rewrite scalept_sum; apply eq_big=>// j _.
+  rewrite scalept_sum//; apply eq_big=>// j _.
   rewrite /h /= fdistmapE.
   have -> : (\sum_(a in {: 'I_n * 'I_m} |
                    a \in preim (@unsplit_prod _ m) (pred1 (Ordinal (unsplit_prodp i j))))
               (fdist_prod d (fun=> e)) a =
              \sum_(a in {: 'I_n * 'I_m} | a \in pred1 (i, j))
-              (fdist_prod d (fun=> e)) a)%coqR.
+              (fdist_prod d (fun=> e)) a)%R.
      apply eq_big=>// k; congr andb; rewrite 3!inE.
      by apply: (eqtype.inj_eq _ k (i, j)); exact: (can_inj (@unsplit_prodK _ _)).
-  rewrite (big_pred1 (i, j))// fdist_prodE/= ssrR.mulRC; congr (scalept _ (S1 (g _))).
+  rewrite (big_pred1 (i, j))// fdist_prodE/= mulrC; congr (scalept _ (S1 (g _))).
   by move: (unsplit_prodK (i, j)) => /(congr1 Datatypes.fst)/esym.
 rewrite (exchange_big_dep xpredT)//=; apply: eq_bigr => j _.
-rewrite -(scale1pt (scalept _ _)) scaleptA// -[(1 * e j)%coqR]/(1 * e j) -(FDist.f1 d).
+rewrite -(scale1pt (scalept _ _)) scaleptA// -(FDist.f1 d).
 rewrite mulr_suml.
-
-have @h : nneg_fun 'I_n.
-(* BUG HB.pack *)
-   exists (fun i => d i * e j)%coqR => i.
-   by apply: ssrR.mulR_ge0.
+pose h x := d x * e j.
+have h0 x : 0 <= h x by rewrite /h mulr_ge0.
 under eq_bigr => i _ do rewrite -[d i * e j]/(h i).
-rewrite scalept_sum; apply: eq_big => // i _.
+rewrite scalept_sum//; apply: eq_big => // i _.
 rewrite /h/= fdistmapE.
 have -> : (\sum_(a in {: 'I_n * 'I_m} |
    a \in preim (unsplit_prod (n:=m)) (pred1 (Ordinal (unsplit_prodp i j))))
           (fdist_prod d (fun=> e)) a =
    \sum_(a in
    {: 'I_n * 'I_m} | a \in pred1 (i, j))
-       (FDist.f (fdist_prod d (fun=> e))) a)%coqR.
+       (FDist.f (fdist_prod d (fun=> e))) a)%R.
    apply: eq_big=>// k; congr andb; rewrite 3!inE.
    by apply: (eqtype.inj_eq _ k (i, j)); exact (can_inj (@unsplit_prodK _ _)).
 rewrite (big_pred1 (i, j))// fdist_prodE/=; congr (scalept _ (S1 (f _))).
@@ -121,7 +120,7 @@ Qed.
 End C.
 
 Section face.
-Variable E : convType.
+Variable E : convType R.
 
 Local Open Scope fun_scope.
 Local Open Scope ring_scope.
@@ -157,7 +156,7 @@ Import LmoduleConvex.
 Let linear_is_affine: affine f.
 Proof. by move=>p x y; rewrite linearD 2!linearZZ. Qed.
 
-#[export] HB.instance Definition _ := isAffine.Build _ _ _ linear_is_affine.
+#[export] HB.instance Definition _ := isAffine.Build _ _ _ _ linear_is_affine.
 
 End linear_affine.
 End LinearAffine.
@@ -174,7 +173,7 @@ Local Open Scope convex_scope.
 Lemma probinvn1 : probinvn 1 = (1 / 2%R : R)%:pr.
 Proof.
 apply: val_inj => /=.
-by rewrite div1R.
+by rewrite div1r.
 Qed.
 
 Lemma onem_half: onem 2^-1 = 2^-1 :> R.
@@ -191,7 +190,6 @@ Lemma ext_carac (A : {convex_set E}) (x: E): x \in A -> [<-> x \in ext A;
 Proof.
 move=>xA.
 have ne20: (2 : R) != 0.
-  rewrite [X in X != _](_ : _ = 2%:R)//.
   by rewrite pnatr_eq0.
 have ge20: (0 : R) <= 2.
   by rewrite ler0n.
@@ -209,12 +207,11 @@ split.
       apply val_inj=>/=.
       set tmp : R := (1 + 1)%:R.
       rewrite (_ : tmp = 2%R)//.
-      rewrite coqRE.
       by rewrite onem_half.
       move: xe=> -> + _.
       move=> /(congr1 (fun x => 2 *: x)).
       rewrite scalerDr probinvn1/=.
-      rewrite div1R coqRE.
+      rewrite div1r.
       rewrite onem_half 2!scalerA divff// 2!scale1r.
       by rewrite scaler_nat mulr2n =>/addrI/esym.
 split.
@@ -242,9 +239,7 @@ split.
       rewrite/= p_of_rsE/=.
       have tE: (2*(Prob.p t : R))/2 = Prob.p t.
          by rewrite mulrAC divff// mul1r.
-      rewrite -{2}tE.
-      congr Rdefinitions.RbaseSymbolsImpl.Rmult.
-      by rewrite coqRE//.
+      by rewrite -{2}tE.
    have wA: u <| Prob.mk t01 |> v \in A.
       by apply mem_set; move:(convex_setP A)=>/asboolP; apply.
    move: vA=>/mem_set vA /(_ wA vA xE) /(congr1 (fun x => x-v)).
@@ -288,7 +283,7 @@ Definition supporting_hyperplane (A : set E) (f: {linear E -> R^o}) (a: R) :=
   (exists x, x \in A /\ f x = a) /\
   ((forall x, x \in A -> f x <= a) \/ (forall x, x \in A -> a <= f x)).
 
-Lemma is_convex_set_preimage [T U : convType] (f : {affine T -> U}) (A : {convex_set U}) :
+Lemma is_convex_set_preimage [T U : convType R] (f : {affine T -> U}) (A : {convex_set U}) :
   is_convex_set (f @^-1` A)%classic.
 Proof.
 apply/asboolP=>x y p/= Ax Ay.
@@ -373,7 +368,7 @@ Local Open Scope ring_scope.
 Local Open Scope convex_scope.
 
 Definition cone0 (A : set E) :=
-  ([set (t : R) *: a | t in (@setT Rpos) & a in A] `<=` A)%classic.
+  ([set t%:num *: a | t in (@setT {posnum R}) & a in A] `<=` A)%classic.
 
 Definition cone (x: E) (A: set E) := cone0 [set a - x | a in A]%classic.
 
@@ -381,18 +376,18 @@ Lemma cone0_convex (A: set E): cone0 A ->
   (is_convex_set A <-> ([set a+b | a in A & b in A] `<=` A)%classic).
 Proof.
 have ne20: (2 : R) != 0.
-  rewrite [X in X != _](_ : _ = 2%:R)//.
   by rewrite pnatr_eq0.
 have gt20 : ((0 : R) < 2)%R.
   by rewrite ltr0n.
 move=>Acone; split=>Aconv.
    move=>x [u uA] [v vA] <-.
-   have uA2: A (2 *: u) by apply Acone; exists (Rpos.mk gt20)=>//; exists u.
-   have vA2: A (2 *: v) by apply Acone; exists (Rpos.mk gt20)=>//; exists v.
+   have uA2: A (2 *: u).
+     by apply: Acone => /=; exists 2%:pos => //; exists u.
+   have vA2: A (2 *: v) by apply Acone; exists 2%:pos =>//; exists v.
    move:Aconv=>/asboolP/(_ _ _ (probinvn 1) uA2 vA2); congr A.
    rewrite probinvn1/=.
    rewrite /conv/=.
-   rewrite div1R coqRE.
+   rewrite div1r.
    by rewrite onem_half 2!scalerA mulVf// 2!scale1r.
 apply/asboolP.
 move=>x y t xA yA.
@@ -402,42 +397,44 @@ move=> t0; move: (prob_le1 t); rewrite -subr_ge0 le0r=>/orP; case.
    by rewrite subr_eq0 /conv/= =>/eqP <-; rewrite onem1 scale0r addr0 scale1r.
 move=> t1; apply Aconv; exists ((Prob.p t : R) *: x);
    [| exists ((onem t) *: y) ]=>//; apply Acone.
-  by exists (Rpos.mk t0)=>//; exists x.
-by exists (Rpos.mk t1)=>//; exists y.
+  by exists (PosNum t0) =>//; exists x.
+by exists (PosNum t1)=>//; exists y.
 Qed.
 
 (* Note: cone0_of A is NOT pointed due to lemma cone0_of_convE. *)
 (* TODO: maybe change the 0 <= k i to 0 < k i in the definition of conv. *)
 
-Definition cone0_of (A: set E): set E := [set a | exists n (s : 'I_n.+1 -> E) (k: 'I_n.+1 -> Rpos),
-  \sum_i (k i : R) *: (s i) = a /\ (range s `<=` A)%classic].
+Definition cone0_of (A: set E) : set E :=
+  [set a | exists n (s : 'I_n.+1 -> E) (k: 'I_n.+1 -> {posnum R}),
+    \sum_i (k i)%:num *: (s i) = a /\ (range s `<=` A)%classic].
 
 Lemma cone0_of_cone0 (A: set E): cone0 (cone0_of A).
 Proof.
 move=>x [t /= _] [a [n [s [k [<- sA]]]]] <-.
-rewrite scaler_sumr; exists n, s, (fun i => mulRpos t (k i)); split => //.
+rewrite scaler_sumr; exists n, s, (fun i => (t%:num * (k i)%:num)%:pos); split => //.
 by apply congr_big=>// i _; apply /esym; apply scalerA.
 Qed.
 
-Lemma cone0_of_hullE (A: set E): cone0_of A = [set (t : R) *: a | t in (@setT Rpos) & a in (hull A)]%classic.
+Lemma cone0_of_hullE (A : set E) :
+  cone0_of A = [set t%:num *: a | t in (@setT {posnum R}) & a in (hull A)]%classic.
 Proof.
 rewrite eqEsubset; split=>x.
-   move=>[n [s [k [<- kA]]]]; set t := \sum_i (k i : R).
-   have k0' (i : 'I_n.+1) : true -> 0 <= (k i : R) by move=> _; apply/ltW/RltP/Rpos_gt0.
+   move=>[n [s [k [<- kA]]]]; set t := \sum_i (k i)%:num.
+   have k0' (i : 'I_n.+1) : true -> 0 <= (k i)%:num by move=> _; apply/ltW.
    have: 0 <= t by apply sumr_ge0.
    rewrite le0r=>/orP; case.
-      move=>/eqP /psumr_eq0P; move=> /(_ k0') /(_ ord0 Logic.eq_refl) k00; exfalso.
-      by move:(Rpos_gt0 (k ord0))=>/RltP; rewrite k00 ltxx.
+      move=>/eqP /psumr_eq0P; move=> /(_ k0') /(_ ord0 Logic.eq_refl) /eqP.
+      by rewrite gt_eqF.
    move=>t0.
-   have tk0: forall i, (Rdefinitions.IZR BinNums.Z0 <= [ffun i => t^-1 * k i] i).
-      by move=>i; rewrite ffunE; apply/mulr_ge0; [ apply ltW; rewrite invr_gt0 | apply k0' ].
-   have tk1 : \sum_(i < n.+1) [ffun i => t^-1 * k i] i = 1.
-      transitivity (\sum_(i < n.+1) t^-1 * k i).
+   have tk0 i : (Rdefinitions.IZR BinNums.Z0 <= [ffun i => t^-1 * (k i)%:num] i).
+      by rewrite ffunE; apply/mulr_ge0; [ apply ltW; rewrite invr_gt0 | apply k0' ].
+   have tk1 : \sum_(i < n.+1) [ffun i => t^-1 * (k i)%:num] i = 1.
+      transitivity (\sum_(i < n.+1) t^-1 * (k i)%:num).
          by apply congr_big=>// i _; rewrite ffunE.
       rewrite -mulr_sumr mulrC divff//.
       by move:t0; rewrite lt0r=>/andP[].
-   move:(t0)=> t0'; exists (Rpos.mk t0')=>//; exists (t^-1 *: \sum_i (k i : R) *: s i).
-      exists n.+1, s, (@FDist.make _ _ (finfun (fun i=> t^-1 * k i)) tk0 tk1); split=> //.
+   move:(t0)=> t0'; exists (PosNum t0')=>//; exists (t^-1 *: \sum_i (k i)%:num *: s i).
+      exists n.+1, s, (@FDist.make _ _ (finfun (fun i=> t^-1 * (k i)%:num)) tk0 tk1); split=> //.
       rewrite scaler_sumr avgnrE.
       apply congr_big=>// i _.
       by rewrite scalerA ffunE.
@@ -445,7 +442,7 @@ rewrite eqEsubset; split=>x.
 move=>[t /= _] [a [n [s [d [sA ->]]]]] <-.
 rewrite avgnrE scaler_sumr.
 rewrite (@bigID_idem _ _ _ _ _ _ (fun i=> 0 < d i))/=; [| exact: addr0].
-have ->: \sum_(i | true && ~~ (0 < d i)) (t : R) *: (d i *: s i) = \sum_(i | true && ~~ (0 < d i)) 0 *: 0.
+have ->: \sum_(i | true && ~~ (0 < d i)) t%:num *: (d i *: s i) = \sum_(i | true && ~~ (0 < d i)) 0 *: 0.
    apply congr_big=>// i /andP [_]; rewrite lt0r negb_and negbK.
    move:(FDist.ge0 d i)=>->; rewrite orbF=>/eqP->.
    by rewrite 2!scale0r GRing.scaler0.
@@ -459,7 +456,7 @@ case: I HeqI=> [| i I] HeqI.
       2: by rewrite -mulr_sumr mul0r.
    apply congr_big=>// i /= dile; move: (FDist.ge0 d i); rewrite le0r.
    rewrite (negbTE dile) orbF => /eqP ->.
-   by rewrite mul0R.
+   by rewrite mul0r.
 have: subseq (i::I) (index_enum 'I_n) by rewrite -HeqI; apply filter_subseq.
 case: n s d sA i I HeqI=> [| n] s d sA i I HeqI.
    by inversion i.
@@ -467,8 +464,9 @@ move=> /subseq_incl; move=> /(_ ord0); rewrite size_index_enum card_ord; move=>
 rewrite /cone0_of/=.
 exists (size I), (s \o (nth ord0 (i :: I))).
 simple refine (ex_intro _ _ _).
-   move=>j; apply (mulRpos t).
-   simple refine (Rpos.mk _).
+   move=> j.
+   apply: (fun x : {posnum R} => (t%:num * x%:num)%:pos).
+   simple refine (PosNum _).
       exact (d (nth ord0 (i :: I) j)).
    rewrite -HeqI.
    apply/(@nth_filter _ (fun i=> 0 < d i)).
@@ -483,7 +481,7 @@ split.
 move=>+/= [j] _ <- =>_.
 by apply sA; eexists.
 Qed.
-      
+
 Lemma cone0_of_sub_cone0_convex (A: set E) (B: {convex_set E}) :
   (A `<=` B -> cone0 B -> cone0_of A `<=` B)%classic.
 Proof.
@@ -496,9 +494,8 @@ End cone.
 
 
 Section Fun.
-
-Variable E: convType.
-Variable f: E -> \bar R.
+Variable E : convType R.
+Variable f : E -> \bar R.
 
 Local Open Scope fun_scope.
 Local Open Scope ring_scope.
@@ -540,7 +537,7 @@ have fle: (Prob.p t)%:E * f u + (onem (Prob.p t))%:E * f v <= f (u <|t|> v).
       - by rewrite addrCA subrr addr0 mul1e.
       - by apply ltW.
       - by rewrite subr_ge0; apply/prob_le1.
-   apply (@lee_add R); rewrite (@lee_pmul2l R)//= lte_fin.
+   apply: leeD; rewrite (@lee_pmul2l R)//= lte_fin.
    by rewrite subr_gt0.
 by move=>/(Order.POrderTheory.le_lt_trans fle); rewrite ltxx.
 Qed.
diff --git a/theories/encompass.v b/theories/encompass.v
index b5dc593..ea9c1e7 100644
--- a/theories/encompass.v
+++ b/theories/encompass.v
@@ -1,5 +1,5 @@
-From mathcomp Require Import all_ssreflect all_algebra vector reals ereal classical_sets.
-From mathcomp Require Import zmodp.
+From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import reals ereal classical_sets.
 Require Export preliminaries preliminaries_hull axiomsKnuth.
 
 (******************************************************************************)
diff --git a/theories/general_position.v b/theories/general_position.v
index 58cc898..1e4ce09 100644
--- a/theories/general_position.v
+++ b/theories/general_position.v
@@ -17,91 +17,91 @@ Section working_environment.
 
 Variable R : realFieldType.
 
-(* Notation prefix, dupplicated from cells_alg.v *)
-Notation pt := (pt (RealField.sort R)).
-Notation p_x := (p_x (RealField.sort R)).
-Notation p_y := (p_y (RealField.sort R)).
-Notation Bpt := (Bpt (RealField.sort R)).
+(* Notation prefix, duplicated from cells_alg.v *)
+Notation pt := (pt (Num.RealField.sort R)).
+Notation p_x := (p_x (Num.RealField.sort R)).
+Notation p_y := (p_y (Num.RealField.sort R)).
+Notation Bpt := (Bpt (Num.RealField.sort R)).
 Notation edge := (edge R).
 Notation left_pt := (@left_pt R).
 Notation right_pt := (@right_pt R).
-Notation event := (event (RealField.sort R) edge).
-Notation outgoing := (outgoing (RealField.sort R) edge).
-Notation point := (point (RealField.sort R) edge).
-Notation cell := (cell (RealField.sort R) edge).
+Notation event := (event (Num.RealField.sort R) edge).
+Notation outgoing := (outgoing (Num.RealField.sort R) edge).
+Notation point := (point (Num.RealField.sort R) edge).
+Notation cell := (cell (Num.RealField.sort R) edge).
 
-Notation dummy_pt := (dummy_pt (RealField.sort R) 1).
-Notation dummy_edge := (dummy_edge (RealField.sort R) 1 edge (@unsafe_Bedge _)).
+Notation dummy_pt := (dummy_pt (Num.RealField.sort R) 1).
+Notation dummy_edge := (dummy_edge (Num.RealField.sort R) 1 edge (@unsafe_Bedge _)).
 Notation dummy_cell :=
-  (dummy_cell (RealField.sort R) 1 edge (@unsafe_Bedge _)).
-Notation dummy_event := (dummy_event (RealField.sort R) 1 edge).
+  (dummy_cell (Num.RealField.sort R) 1 edge (@unsafe_Bedge _)).
+Notation dummy_event := (dummy_event (Num.RealField.sort R) 1 edge).
 Notation edge_below :=
-  (generic_trajectories.edge_below (RealField.sort R) eq_op <=%R +%R
+  (generic_trajectories.edge_below (Num.RealField.sort R) eq_op <=%R +%R
     (fun x y => x - y) *%R 1 edge left_pt right_pt).
 Notation "x <| y" := (edge_below x y).
 Notation valid_edge :=
-  (generic_trajectories.valid_edge (RealField.sort R)
-   le edge left_pt right_pt).
+  (generic_trajectories.valid_edge (Num.RealField.sort R)
+   <=%R edge left_pt right_pt).
 Notation vertical_intersection_point :=
-  (vertical_intersection_point (RealField.sort R)
-  le +%R (fun x y => x - y) *%R
+  (vertical_intersection_point (Num.RealField.sort R)
+  <=%R +%R (fun x y => x - y) *%R
   (fun x y => x / y) edge left_pt right_pt).
 Notation point_under_edge :=
-  (point_under_edge (RealField.sort R) le +%R (fun x y => x - y) *%R 1
+  (point_under_edge (Num.RealField.sort R) <=%R +%R (fun x y => x - y) *%R 1
   edge left_pt right_pt).
 Notation "p <<= g" := (point_under_edge p g).
 Notation "p >>> g" := (~~ (point_under_edge p g)).
 Notation point_strictly_under_edge :=
-  (point_strictly_under_edge  (RealField.sort R) eq_op <=%R +%R
+  (point_strictly_under_edge  (Num.RealField.sort R) eq_op <=%R +%R
   (fun x y => x - y) *%R 1 edge left_pt right_pt).
 Notation "p <<< g" := (point_strictly_under_edge p g).
 Notation "p >>= g" := (~~ (point_strictly_under_edge p g)).
 
 Notation contains_point :=
-  (contains_point (RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R 1
+  (contains_point (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R 1
     edge left_pt right_pt).
 
 Notation open_cells_decomposition_contact :=
-  (open_cells_decomposition_contact (RealField.sort R) eq_op le +%R
+  (open_cells_decomposition_contact (Num.RealField.sort R) eq_op <=%R +%R
   (fun x y => x - y) *%R 1 edge left_pt right_pt).
 Notation open_cells_decomposition_rec :=
-  (open_cells_decomposition_rec (RealField.sort R) eq_op le +%R
+  (open_cells_decomposition_rec (Num.RealField.sort R) eq_op <=%R +%R
   (fun x y => x - y) *%R 1 edge (@unsafe_Bedge R) left_pt
   right_pt).
 Notation open_cells_decomposition :=
-  (open_cells_decomposition (RealField.sort R) eq_op le +%R
+  (open_cells_decomposition (Num.RealField.sort R) eq_op <=%R +%R
   (fun x y => x - y) *%R 1 edge (@unsafe_Bedge R) left_pt
   right_pt).
 
-Notation scan_state := (scan_state (RealField.sort R) edge).
-Notation sc_open1 := (sc_open1 (RealField.sort R) edge).
-Notation lst_open := (lst_open (RealField.sort R) edge).
-Notation sc_open2 := (sc_open2 (RealField.sort R) edge).
-Notation sc_closed := (sc_closed (RealField.sort R) edge).
-Notation lst_closed := (lst_closed (RealField.sort R) edge).
+Notation scan_state := (scan_state (Num.RealField.sort R) edge).
+Notation sc_open1 := (sc_open1 (Num.RealField.sort R) edge).
+Notation lst_open := (lst_open (Num.RealField.sort R) edge).
+Notation sc_open2 := (sc_open2 (Num.RealField.sort R) edge).
+Notation sc_closed := (sc_closed (Num.RealField.sort R) edge).
+Notation lst_closed := (lst_closed (Num.RealField.sort R) edge).
 
 Notation update_closed_cell :=
-  (update_closed_cell (RealField.sort R) 1 edge).
+  (update_closed_cell (Num.RealField.sort R) 1 edge).
 
 Notation set_left_pts :=
-  (set_left_pts (RealField.sort R) edge).
+  (set_left_pts (Num.RealField.sort R) edge).
 
-Notation low := (low (RealField.sort R) edge).
-Notation high := (high (RealField.sort R) edge).
-Notation left_pts := (left_pts (RealField.sort R) edge).
-Notation right_pts := (right_pts (RealField.sort R) edge).
-Notation Bcell := (Bcell (RealField.sort R) edge).
+Notation low := (low (Num.RealField.sort R) edge).
+Notation high := (high (Num.RealField.sort R) edge).
+Notation left_pts := (left_pts (Num.RealField.sort R) edge).
+Notation right_pts := (right_pts (Num.RealField.sort R) edge).
+Notation Bcell := (Bcell (Num.RealField.sort R) edge).
 Notation cell_center :=
-  (cell_center (RealField.sort R) +%R (fun x y => x / y) 1%:R edge).
+  (cell_center (Num.RealField.sort R) +%R (fun x y => x / y) 1%:R edge).
 
 Notation closing_cells :=
-  (generic_trajectories.closing_cells (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (generic_trajectories.closing_cells (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
     *%R (fun x y => x / y) edge left_pt right_pt).
 Notation close_cell :=
-  (generic_trajectories.close_cell (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (generic_trajectories.close_cell (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
     *%R (fun x y => x / y) edge left_pt right_pt).
 
-Notation set_pts := (set_pts (RealField.sort R) edge).
+Notation set_pts := (set_pts (Num.RealField.sort R) edge).
 
 (* This function is to be called only when the event is in the middle
   of the last opening cell.  The point e needs to be added to the left
@@ -109,27 +109,27 @@ Notation set_pts := (set_pts (RealField.sort R) edge).
   the first segment of the last opening cells should keep its existing
   left points.*)
 Notation update_open_cell :=
-  (update_open_cell (RealField.sort R) eq_op le +%R (fun x y => x - y)
+  (update_open_cell (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
   *%R (fun x y => x / y) 1 edge (@unsafe_Bedge R) left_pt right_pt).
 
 Notation update_open_cell_top :=
-  (update_open_cell_top (RealField.sort R) eq_op le +%R (fun x y => x - y)
+  (update_open_cell_top (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
   *%R (fun x y => x / y) 1
   edge (@unsafe_Bedge R) left_pt right_pt).
 
-Notation Bscan := (Bscan (RealField.sort R) edge).
+Notation Bscan := (Bscan (Num.RealField.sort R) edge).
 
 Notation opening_cells_aux :=
-  (opening_cells_aux (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (opening_cells_aux (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
   *%R (fun x y => x / y) 1 edge (@unsafe_Bedge R) left_pt right_pt).
 
 Notation simple_step :=
-  (generic_trajectories.simple_step (RealField.sort R) eq_op le +%R
+  (generic_trajectories.simple_step (Num.RealField.sort R) eq_op <=%R +%R
   (fun x y => x - y) *%R (fun x y => x / y)
   1 edge (@unsafe_Bedge R) left_pt right_pt).
 
 Notation step :=
-  (step (RealField.sort R) eq_op le +%R (fun x y => x - y) *%R
+  (step (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R
   (fun x y => x / y) 1 edge (@unsafe_Bedge R) left_pt right_pt).
 (*
 Definition scan events st : seq cell * seq cell :=
@@ -138,7 +138,7 @@ Definition scan events st : seq cell * seq cell :=
    lst_closed final_state :: sc_closed final_state). *)
 
 Notation start_open_cell :=
-  (start_open_cell (RealField.sort R) eq_op le +%R (fun x y => x - y)
+  (start_open_cell (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
   *%R (fun x y => x / y) edge left_pt right_pt).
 
 Notation open_cell_side_limit_ok :=
@@ -157,8 +157,9 @@ Notation open_cell_side_limit_ok :=
   cells, here named "open", should be reduced to only one element. *)
 
 Record common_general_position_invariant bottom top edge_set s
-  (events : seq event) :=
-  { gcomm : common_invariant bottom top edge_set s events;
+  (all_events processed_events events : seq event) :=
+  { gcomm : common_invariant bottom top edge_set s all_events processed_events
+    events;
    general_pos :
      all (fun ev => lst_x _ _ s < p_x (point ev)) events &&
      sorted (fun e1 e2 => p_x (point e1) < p_x (point e2)) events;
@@ -166,20 +167,21 @@ Record common_general_position_invariant bottom top edge_set s
 
 Record disjoint_general_position_invariant (bottom top : edge)
  (edge_set : seq edge)
- (s : scan_state) (events : seq event) :=
+ (s : scan_state) (all_events processed_events events : seq event) :=
  { op_cl_dis :
      {in state_open_seq s & state_closed_seq s,
        disjoint_open_closed_cells R};
    cl_dis : {in state_closed_seq s &, disjoint_closed_cells R};
    common_inv_dis : common_general_position_invariant bottom top
-        edge_set s events;
+        edge_set s all_events processed_events events;
    pairwise_open : pairwise edge_below
        (bottom :: [seq high c | c <- state_open_seq s]);
    closed_at_left :
        {in state_closed_seq s & events,
           forall c e, right_limit c <= p_x (point e)}}.
 
-Lemma initial_common_general_position_invariant bottom top s events:
+Lemma initial_common_general_position_invariant bottom top s 
+  events:
   sorted (fun e1 e2=> p_x (point e1) < p_x (point e2)) events ->
   bottom <| top ->
   (* TODO: rephrase this statement in a statement that easier to understand. *)
@@ -193,7 +195,8 @@ Lemma initial_common_general_position_invariant bottom top s events:
   close_edges_from_events events ->
   events != [::] ->
   common_general_position_invariant bottom top s
-    (initial_state bottom top events) (behead events).
+    (initial_state bottom top events)
+    events (take 1 events) (behead events).
 Proof.
 move=> ltev boxwf startok nocs' evin lexev evsub out_evs uniqout cle evsn0.
 have ici := initial_common_invariant boxwf startok nocs' evin lexev evsub
@@ -222,8 +225,7 @@ Lemma initial_disjoint_general_position_invariant
   close_edges_from_events events ->
   events != [::] ->
   disjoint_general_position_invariant bottom top s
-   (initial_state bottom top events)
-   (* (head (dummy_event _) events) *) (behead events).
+   (initial_state bottom top events) events (take 1 events) (behead events).
 Proof.
 move=> ltev boxwf startok nocs' evin lexev evsub out_evs uniqout cle evsn0.
 have := initial_common_general_position_invariant ltev boxwf startok
@@ -270,7 +272,7 @@ Qed.
 
 Lemma simple_step_common_general_position_invariant
   bottom top s fop lsto lop fc cc lcc lc le he cls lstc ev
-  lsthe lstx evs :
+  lsthe lstx all_events processed_events evs :
   bottom <| top ->
   {in bottom :: top :: s &, forall e1 e2, inter_at_ext e1 e2} ->
   {in s, forall g, inside_box bottom top (left_pt g) &&
@@ -278,10 +280,11 @@ Lemma simple_step_common_general_position_invariant
   open_cells_decomposition (fop ++ lsto :: lop) (point ev) =
     (fc, cc, lcc, lc, le, he) ->
   common_general_position_invariant bottom top s
-     (Bscan fop lsto lop cls lstc lsthe lstx)
+     (Bscan fop lsto lop cls lstc lsthe lstx) all_events processed_events
      (ev :: evs) ->
   common_general_position_invariant bottom top s
-     (simple_step fc cc lc lcc le he cls lstc ev)
+     (simple_step fc cc lc lcc le he cls lstc ev) all_events
+     (rcons processed_events ev)
     evs.
 Proof.
 move=> boxwf nocs' inbox_s oe.
@@ -316,7 +319,7 @@ Qed.
 
 Lemma simple_step_disjoint_general_position_invariant
   bottom top s fop lsto lop fc cc lcc lc le he cls lstc ev
-  lsthe lstx evs :
+  lsthe lstx all_events processed_events evs :
   bottom <| top ->
   {in bottom :: top :: s &, forall e1 e2, inter_at_ext e1 e2} ->
   {in s, forall g, inside_box bottom top (left_pt g) &&
@@ -324,18 +327,19 @@ Lemma simple_step_disjoint_general_position_invariant
   open_cells_decomposition (fop ++ lsto :: lop) (point ev) =
     (fc, cc, lcc, lc, le, he) ->
   disjoint_general_position_invariant bottom top s
-     (Bscan fop lsto lop cls lstc lsthe lstx)
+     (Bscan fop lsto lop cls lstc lsthe lstx) all_events processed_events
      (ev :: evs) ->
   disjoint_general_position_invariant bottom top s
-     (simple_step fc cc lc lcc le he cls lstc ev)
+     (simple_step fc cc lc lcc le he cls lstc ev) all_events
+     (rcons processed_events ev)
     evs.
 Proof.
 move=> boxwf nocs' inbox_s oe.
 move=> []; rewrite /state_open_seq/state_closed_seq/=.
 move=> oc_dis c_dis Cinv pw rl.
 have := Cinv=> -[] []; rewrite /state_open_seq/state_closed_seq/=.
-move=> inv1 lstxq lstheq sub_edges cle out_es uniqout inbox_es.
-move=> no_dup lexev oks gen_pos.
+move=> inv1 lstxq lstheq sub_edges events_dec cle out_es uniqout inbox_es.
+move=> no_dup lexev oks _ _ _.
 have := inv1 => -[] clae [] []; first by [].
 move=> sval []adj []cbtom rfo.
 rewrite /simple_step.
@@ -343,7 +347,8 @@ case oca_eq : (opening_cells_aux _ _ _ _) => [nos lno].
 have Cinv' : common_general_position_invariant bottom top s
          (Bscan (fc ++ nos) lno lc
             (cls ++ lstc :: closing_cells (point ev) cc)
-            (close_cell (point ev) lcc) he (p_x (point ev))) evs.
+            (close_cell (point ev) lcc) he (p_x (point ev)))
+            all_events (rcons processed_events ev) evs.
   have := simple_step_common_general_position_invariant boxwf nocs' inbox_s oe.
   rewrite /simple_step.
   by rewrite oca_eq=> /(_ _ _ lsthe lstx); apply.
@@ -351,9 +356,9 @@ have cl_at_left' : {in rcons cls lstc,
         forall c, right_limit c <= p_x (point ev)}.
   by move=> c cin; apply: rl; rewrite // inE eqxx.
 have oute : out_left_event ev by apply: out_es; rewrite inE eqxx.
-have := step_keeps_disjoint_default inbox_es oute rfo
+have disjointness := step_keeps_disjoint_default inbox_es oute rfo
          cbtom adj sval pw oks oc_dis c_dis cl_at_left'.
-rewrite oe oca_eq /= !cat_rcons -!cats1 /= => disjointness.
+rewrite oe oca_eq /= !cat_rcons -!cats1 /= in disjointness.
 have op_cl_dis':
   {in (fc ++ nos) ++ lno :: lc & rcons (cls ++ lstc ::
            closing_cells (point ev) cc) (close_cell (point ev) lcc),
@@ -370,8 +375,7 @@ have noc : {in all_edges (fop ++ lsto :: lop) (ev :: evs) &,
   by move=> g1 gt2 g1in g2in; apply: nocs; apply: sub_edges.
 have pwo' : pairwise edge_below
            (bottom :: [seq high c | c <- (fc ++ nos) ++ lno :: lc]).
-have := step_keeps_pw_default inbox_es oute rfo cbtom adj sval
-      noc pw.
+  have := step_keeps_pw_default inbox_es oute rfo cbtom adj sval noc pw.
   by rewrite oe oca_eq -catA.
 have right_limit_closed' :
   {in  rcons(cls ++
@@ -380,6 +384,8 @@ have right_limit_closed' :
   have:= step_keeps_right_limit_closed_default inbox_es cbtom adj
     sval lexev cl_at_left'.
   by rewrite oe oca_eq /=.
+have all_events_break' : all_events = rcons processed_events ev ++ evs.
+  by rewrite cat_rcons.
 by constructor.
 Qed.
 
@@ -413,18 +419,21 @@ have := initial_disjoint_general_position_invariant ltev boxwf startok nocs'
   evin lexev evsub out_evs uniq_evs cle evsn0.
 rewrite /initial_state evsq.
 case oca_eq : (opening_cells_aux _ _ _ _) => [nos1 lno1] /=.
-elim: (future_events) {oca_eq evsq} (Bscan _ _ _ _ _ _ _)=> [ | ev' fut' Ih].
+have : ev :: future_events = (ev :: take 0 future_events) ++ future_events.
+  by case: (future_events).
+move: (ev :: future_events) (ev :: take 0 future_events).
+elim: (future_events) {oca_eq evsq} (Bscan _ _ _ _ _ _ _)=> [ | ev' fut' Ih] + ae pe.
   move=> state_f /=; case: state_f=> [] f m l cls lstc lsthe lstx.
-  move=> /[swap] -[] <- <-; case; rewrite /state_open_seq /state_closed_seq /=.
+  move=> aeq /[swap] -[] <- <-; case; rewrite /state_open_seq /state_closed_seq /=.
   move=> dis_op_cl dis_cl *; split; move=> c1 c2 c1in c2in.
     by apply: dis_cl; rewrite // mem_rcons.
   by apply: dis_op_cl; rewrite // mem_rcons.
 move=> {evs ltev evin lexev evsub out_evs uniq_evs cle evsn0}.
-move=> [fop lsto lop cls lstc lsthe lstx].
+move=> [fop lsto lop cls lstc lsthe lstx] aeq.
 case; set ops' := (state_open_seq _); set (cls' := state_closed_seq _).
 rewrite /=.
 move=> dis_open_closed dis_cl /[dup] Cinv [] [] inv1 lstxq lstheq sub_edges.
-move=> /[dup] cle /andP[cl_e_fut' cle'] out_fut'.
+move=> all_events_dec /[dup] cle /andP[cl_e_fut' cle'] out_fut'.
 move=> uniq_evs'.
 move=> /= /[dup]  inbox_all_events' /andP[inbox_e inbox_all_events].
 move=> no_dup lexevs oks.
@@ -440,7 +449,8 @@ rewrite -/(open_cells_decomposition _ _).
 rewrite /generic_trajectories.simple_step.
 case oe : (open_cells_decomposition _ _) => [[[[[fc cc] lcc] lc] le] he].
 case oca_eq : (opening_cells_aux _ _ _ _) => [nos lno].
-apply: Ih.
+apply: (Ih _ ae (rcons pe ev')).
+  by rewrite aeq cat_rcons.
 have :=
   simple_step_disjoint_general_position_invariant boxwf nocs' inbox_s oe.
   rewrite /simple_step.
@@ -449,7 +459,7 @@ by apply.
 Qed.
 
 Record edge_covered_general_position_invariant (bottom top : edge)
- (edge_set : seq edge) (processed_set : seq event)
+ (edge_set : seq edge) (all_events processed_set : seq event)
  (s : scan_state) (events : seq event) :=
  { edge_covered_ec : {in processed_set, forall e,
        {in outgoing e, forall g,
@@ -458,7 +468,7 @@ Record edge_covered_general_position_invariant (bottom top : edge)
        exists2 c, c \in (state_closed_seq s) &
            point e \in (right_pts c : seq pt) /\ point e >>> low c}  ;
    common_inv_ec : common_general_position_invariant bottom top edge_set
-     s events;
+     s all_events processed_set events;
    non_in_ec :
       {in edge_set & events, forall g e, non_inner g (point e)};
    inj_high : {in state_open_seq s &, injective high};
@@ -484,7 +494,7 @@ Lemma initial_edge_covering_general_position
   {in events, forall ev, uniq (outgoing ev)} ->
   events != [::] ->
   edge_covered_general_position_invariant bottom top s
-   [:: (head dummy_event events)]
+   events [:: (head dummy_event events)]
    (initial_state bottom top events) (behead events).
 Proof.
 move=> gen_pos lexev wf cle startok nocs' n_inner inbox_es sub_es out_es
@@ -561,7 +571,7 @@ by constructor.
 Qed.
 
 Lemma simple_step_edge_covered_general_position
-  bottom top s cov_set fop lsto lop fc cc lcc lc le he cls lstc ev
+  bottom top s all_events cov_set fop lsto lop fc cc lcc lc le he cls lstc ev
   lsthe lstx evs :
   bottom <| top ->
   {in bottom :: top :: s &, forall e1 e2, inter_at_ext e1 e2} ->
@@ -570,10 +580,10 @@ Lemma simple_step_edge_covered_general_position
   open_cells_decomposition (fop ++ lsto :: lop) (point ev) =
     (fc, cc, lcc, lc, le, he) ->
   edge_covered_general_position_invariant bottom top s
-   cov_set (Bscan fop lsto lop cls lstc lsthe lstx)
+   all_events cov_set (Bscan fop lsto lop cls lstc lsthe lstx)
    (ev :: evs) ->
   edge_covered_general_position_invariant bottom top s
-    (rcons cov_set ev) (simple_step fc cc lc lcc le he cls lstc ev)
+    all_events (rcons cov_set ev) (simple_step fc cc lc lcc le he cls lstc ev)
     evs.
 Proof.
 move=> boxwf nocs' inbox_s.
@@ -584,7 +594,7 @@ move=> oe.
 move=> [] covered p_covered /[dup] Cinv [] [] /[dup] inv_s [] clae.
 move=> - [] []; first by [].
 rewrite /state_open_seq/state_closed_seq /= => sval [] adj [] cbtom rfo.
-move=> lstxq lstheq sub_edges cle out_es uniq_evs.
+move=> lstxq lstheq sub_edges events_dec cle out_es uniq_evs.
 move=> /[dup] inbox0 /andP[] inbox_e inbox_es no_dup lexev oks.
 move=> bottom_left_corner_cond strd.
 move=> /andP[] lstxlt pathlt n_inner inj_high btm_left_lex.
@@ -727,17 +737,17 @@ rewrite /initial_state evsq /=.
 case oca_eq : (opening_cells_aux _ _ _ _) => [nos lno].
 set istate := Bscan _ _ _ _ _ _ _.
 move=> istateP req.
-suff main : forall events op cl st cov_set,
-  edge_covered_general_position_invariant bottom top s cov_set st events ->
+suff main : forall events all_events op cl st cov_set,
+  edge_covered_general_position_invariant bottom top s all_events cov_set st events ->
   scan events st = (op, cl) ->
   ({in events_to_edges (cov_set ++ events), forall g, edge_covered g op cl} /\
   {in cov_set ++ events, forall e, exists2 c, c \in cl &
     point e \in (right_pts c : seq pt) /\ point e >>> low c}).
-  by move: req; apply: (main _ _ _ _ [:: ev]).
-  move=> {req istateP istate oca_eq lno nos evsn0 evsq future_events ev}.
-  move=> {uniq_edges n_inner out_evs evsub lexev evin startok ltev}.
-  move=> {cle closed open evs}.
-  elim=> [ | ev evs Ih] op cl st cov_set.
+  by move: req; apply: (main _ (ev :: future_events) _ _ _ [:: ev]).
+move=> {req istateP istate oca_eq lno nos evsn0 evsq future_events ev}.
+move=> {uniq_edges n_inner out_evs evsub lexev evin startok ltev}.
+move=> {cle closed open evs}.
+elim=> [ | ev evs Ih] all_events op cl st cov_set.
   case: st => fop lsto lop cls lstc lsthe lstx /=.
   move=> []; rewrite /state_open_seq/state_closed_seq /= => + p_main.
   move=> main _ _ _ _ [] <- <-; rewrite cats0; split.
@@ -747,7 +757,7 @@ suff main : forall events op cl st cov_set,
   move=> e=> /p_main [c2 c2in pin2]; exists c2=> //.
   by move: c2in; rewrite mem_rcons.
 move=> inv0; rewrite -cat_rcons.
-apply: Ih.
+apply: (Ih all_events).
 case stq : st => [fop lsto lop cls lstc lsthe lstx].
 rewrite /step/generic_trajectories.step.
 have /andP[/andP[+ _] _] := general_pos (common_inv_ec inv0).
@@ -761,13 +771,14 @@ by have := simple_step_edge_covered_general_position boxwf nocs'
 Qed.
 
 Record safe_side_general_position_invariant (bottom top : edge)
- (edge_set : seq edge) (processed_set : seq event)
+ (edge_set : seq edge) (all_events processed_set : seq event)
  (s : scan_state) (events : seq event) :=
  { disjoint_ss :
-     disjoint_general_position_invariant bottom top edge_set s events;
+     disjoint_general_position_invariant bottom top edge_set s 
+     all_events processed_set events;
    covered_ss :
      edge_covered_general_position_invariant bottom top edge_set
-       processed_set s events;
+       all_events processed_set s events;
     left_proc : {in processed_set & events, forall e1 e2,
                      p_x (point e1) < p_x (point e2)};
     rf_closed : {in state_closed_seq s, forall c, low c <| high c};
@@ -781,7 +792,7 @@ Record safe_side_general_position_invariant (bottom top : edge)
           forall c e, left_limit c < p_x (point e)};
    left_o_b :
         {in state_open_seq s, forall c, left_limit c <
-              min (p_x (right_pt bottom)) (p_x (right_pt top))};
+              Num.min (p_x (right_pt bottom)) (p_x (right_pt top))};
    closed_lt :
         {in state_closed_seq s, forall c, left_limit c < right_limit c};
    closed_ok :
@@ -821,7 +832,7 @@ Lemma initial_safe_side_general_position bottom top s events:
   {in events, forall ev, uniq (outgoing ev)} ->
   events != [::] ->
   safe_side_general_position_invariant bottom top s
-    [::(head dummy_event events)]
+    events [::(head dummy_event events)]
    (initial_state bottom top events) (behead events).
 Proof.
 move=> gen_pos lexev wf cle startok nocs' n_inner inbox_es sub_es out_es
@@ -951,15 +962,16 @@ have lt_p_ev :
   by move=> e1 e2; rewrite inE => /eqP ->; apply: lte.
 have ll_o_b :
   {in nos ++ [:: lno], forall c,
-       left_limit c < min (p_x (right_pt bottom)) (p_x (right_pt top))}.
+       left_limit c < Num.min (p_x (right_pt bottom)) (p_x (right_pt top))}.
   move=> c cin.
   have := opening_cells_left oute vb0 vt0; rewrite /opening_cells oca_eq.
   rewrite -cats1 => /(_ _ cin) ->.
   by apply: inside_box_lt_min_right.
+rewrite [take 1 _](_ : _ = [:: ev]) in d_inv; last first.
+  by case: (evs).
 by constructor.
 Qed.
 
-
 Lemma start_safe_sides bottom top s closed open evs :
   sorted (fun e1 e2=> p_x (point e1) < p_x (point e2)) evs ->
   bottom <| top ->
@@ -991,7 +1003,7 @@ Lemma start_safe_sides bottom top s closed open evs :
     high (head_cell open) = top /\
     {in open & closed, disjoint_open_closed_cells R} /\
     (evs != [::] ->
-      left_limit (head_cell open) < min (p_x (right_pt bottom))
+      left_limit (head_cell open) < Num.min (p_x (right_pt bottom))
       (p_x (right_pt top))).
 Proof.
 move=> ltev boxwf startok nocs' inbox_s evin lexev evsub out_evs cle
@@ -1003,14 +1015,15 @@ case evsq : evs => [ | ev future_events]; first by  move=> [] <- <-.
 have evsn0 : evs != [::] by rewrite evsq.
 case oca_eq : opening_cells_aux => [nos lno].
 set istate := Bscan _ _ _ _ _ _ _.
-have : safe_side_general_position_invariant bottom top s [:: ev]
+have : safe_side_general_position_invariant bottom top s evs [:: ev]
   istate future_events.
   have := initial_safe_side_general_position ltev lexev boxwf cle startok
     nocs' n_inner evin evsub out_evs uniq_edges evsn0.
   by rewrite evsq /= oca_eq.
 move=> invss req.
-suff main: forall events op cl st processed_set,
-  safe_side_general_position_invariant bottom top s processed_set st events ->
+suff main: forall events op cl st all_events processed_set,
+  safe_side_general_position_invariant bottom top s all_events
+    processed_set st events ->
   scan events st = (op, cl) ->
   {in cl, forall c,
     low c <| high c /\
@@ -1029,14 +1042,14 @@ suff main: forall events op cl st processed_set,
   low (head_cell op) = bottom /\
   high (head_cell op) = top /\
   {in op & cl, disjoint_open_closed_cells R} /\
-  (left_limit (head_cell op) < min (p_x (right_pt bottom))
+  (left_limit (head_cell op) < Num.min (p_x (right_pt bottom))
       (p_x (right_pt top))).
-  have [A [B [C [D [E [F [G [H I]]]]]]]] := main _ _ _ _ _ invss req.
+  have [A [B [C [D [E [F [G [H I]]]]]]]] := main _ _ _ _ _ _ invss req.
   split; last by [].
   move=> c cin; move: (A c cin) => [] crf [] difc [] lltr [] clok A'.
   do 4 (split; first by []).
   by move=> p pside; have := A' _ pside.
-elim=> [ | {evsq oca_eq istate invss}ev {req}future_events Ih] op cl st p_set.
+elim=> [ | {evsq oca_eq istate invss}ev {req}future_events Ih] op cl st all_events p_set.
   case stq : st => [fop lsto lop cls lstc lsthe lstx] [].
   move=> d_inv e_inv.
   set c_inv := common_inv_dis d_inv.
@@ -1118,7 +1131,7 @@ rewrite /simple_step/generic_trajectories.simple_step/=.
 rewrite -/(opening_cells_aux _ _ _ _).
 case oca_eq : (opening_cells_aux _ _ _ _) => [{}nos {}lno].
 rewrite -(cat_rcons ev).
-apply: Ih.
+apply: (Ih _ _ _ all_events).
 have [clae [pre_sval [adj [cbtom rfo]]]] := inv1 (gcomm c_inv).
 move: pre_sval=> [| sval]; first by[].
 have inbox_es := inbox_events (gcomm c_inv).
@@ -1138,16 +1151,17 @@ have oute : out_left_event ev.
 have oute' :
   {in (sort edge_below (outgoing ev)), forall g, left_pt g == point ev}.
   by move=> g; rewrite mem_sort; apply: oute.
-set rstate := Bscan _ _ _ _ _ _ _.
+set rstate := Bscan (fc ++ nos) _ _ _ _ _ _.
 have d_inv':
-  disjoint_general_position_invariant bottom top s rstate future_events.
+  disjoint_general_position_invariant bottom top s rstate all_events
+    (rcons p_set ev) future_events.
   move: (d_inv); rewrite stq=> d_inv'.
   have := simple_step_disjoint_general_position_invariant boxwf nocs'
       inbox_s oe d_inv'.
   rewrite /simple_step/generic_trajectories.simple_step/=.
   by rewrite -/(opening_cells_aux _ _ _ _) oca_eq.
 have e_inv' :edge_covered_general_position_invariant bottom top s
-    (rcons p_set ev) rstate future_events.
+    all_events (rcons p_set ev) rstate future_events.
   move: e_inv; rewrite stq=> e_inv.
   have := simple_step_edge_covered_general_position boxwf nocs'
       inbox_s oe e_inv.
@@ -1521,7 +1535,7 @@ have rf_closed1 : {in state_closed_seq rstate, forall c, low c <| high c}.
   move=> [] _ [] _ [] _ [] _ /allP; apply.
   by rewrite ocd -cat_rcons !mem_cat c'in orbT.
 have lo_lb' : {in state_open_seq rstate, forall c,
-               left_limit c < min (p_x (right_pt bottom)) (p_x (right_pt top))}.
+               left_limit c < Num.min (p_x (right_pt bottom)) (p_x (right_pt top))}.
   move=>c; rewrite /state_open_seq/= -catA -cat_rcons !mem_cat orbCA.
   move=> /orP[cnew | cold]; last first.
     by apply: lo_lb; rewrite ocd -cat_rcons !mem_cat orbCA cold orbT.
@@ -1531,4 +1545,4 @@ have lo_lb' : {in state_open_seq rstate, forall c,
 by constructor.
 Qed.
 
-End working_environment.
\ No newline at end of file
+End working_environment.
diff --git a/theories/infra.v b/theories/infra.v
deleted file mode 100644
index 710e47a..0000000
--- a/theories/infra.v
+++ /dev/null
@@ -1,569 +0,0 @@
-From HB Require Import structures.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq order.
-From mathcomp Require Import choice fintype finfun ssrfun bigop ssralg.
-(*Require Import orderedalg.*)
-
-Require Import Zbool.
-(*Require Import QArith.*)
-Require Import Qcanon.
-Require Import ZArith.
-
-Close Scope Q_scope.
-
-Set   Implicit Arguments.
-Unset Strict Implicit.
-
-Import Prenex Implicits.
-
-Import GRing.
-
-Local Open Scope ring_scope.
-
-(* -------------------------------------------------------------------- *)
-(* Various eqtype, subtype, choice, count canonical structures          *)
-(*               from the standard library                              *)
-(* -------------------------------------------------------------------- *)
-
-(* Structures on positive *)
-
-Definition eqp (p q : positive) : bool :=
-  match ((p ?= q))%positive with Eq => true | _ => false end.
-
-Lemma eqpP : Equality.axiom eqp.
-Proof.
-  move=> p q; apply: (iffP  idP)=>[|<-]; last by rewrite /eqp Pos.compare_refl.
-  rewrite /eqp; case e: ((p ?= q))%positive=> // _; exact: Pcompare_Eq_eq.
-Qed.
-
-HB.instance Definition _ := hasDecEq.Build _ eqpP.
-
-Definition p_unpickle n := Some (Pos.pred (P_of_succ_nat n)).
-
-Lemma p_pick_cancel : pcancel nat_of_P p_unpickle.
-Proof.
-  move=> x; rewrite /p_unpickle; congr Some.
-  by rewrite pred_o_P_of_succ_nat_o_nat_of_P_eq_id.
-Qed.
-
-HB.instance Definition _ := @PCanIsCountable _ _ _ _ p_pick_cancel.
-
-(*Canonical Structure p_choiceType :=
-  Eval hnf in ChoiceType positive p_choiceMixin.
-Canonical Structure p_countType :=
-  Eval hnf in CountType positive p_countMixin.*)
-
-(* Structures on Z *)
-
-Lemma eqzP : Equality.axiom Zeq_bool.
-Proof. by move=> z1 z2;  apply: (iffP idP); move/Zeq_is_eq_bool. Qed.
-
-HB.instance Definition _ := hasDecEq.Build _ eqzP.
-
-Definition z_code (z : Z) :=
-  match z with
-    |0%Z => (0%nat, true)
-    |Zpos p => (pickle p, true)
-    |Zneg p => (pickle p, false)
-  end.
-
-Definition z_pickle z := pickle (z_code z).
-
-Definition z_decode c :=
-  match c with
-    |(0%nat, true) => Some 0%Z
-    |(0%nat, false) => None
-    |(n, true) =>
-      if (unpickle n) is Some p then Some (Zpos p) else None
-    |(n, false) =>
-      if (unpickle n) is Some p then Some (Zneg p) else None
-  end.
-
-Definition z_unpickle n :=
-  match (unpickle n) with
-    |None => None
-    |Some u => z_decode u
-  end.
-
-Lemma z_codeK : pcancel z_code z_decode.
-Proof.
-  rewrite /z_code /z_decode.
-  case=> // n; case e : (pickle n)=>[|m]; rewrite -?e ?pickleK //;
-    by move/ltP: (lt_O_nat_of_P n); rewrite -e -[pickle]/nat_of_P ltnn.
-Qed.
-
-Lemma z_pick_cancel : pcancel z_pickle z_unpickle.
-Proof.
-  by move=> x; rewrite /z_pickle /z_unpickle pickleK z_codeK.
-Qed.
-
-HB.instance Definition _ := @PCanIsCountable _ _ _ _ z_pick_cancel.
-
-(*
-Definition z_countMixin  := CountMixin z_pick_cancel.
-Definition z_choiceMixin := CountChoiceMixin z_countMixin.
-
-Canonical Structure z_choiceType :=
-  Eval hnf in ChoiceType Z z_choiceMixin.
-Canonical Structure z_countType :=
-  Eval hnf in CountType Z z_countMixin.
-*)
-
-Lemma ZplusA : associative Zplus.
-Proof. by exact Zplus_assoc. Qed.
-
-Lemma ZplusC : commutative Zplus.
-Proof. by exact Zplus_comm. Qed.
-
-Lemma Zplus0 : left_id (0%Z) Zplus.
-Proof. by exact Zplus_0_l. Qed.
-
-Lemma ZplusNr : left_inverse  0%Z Z.opp Zplus.
-Proof. exact Zplus_opp_l. Qed. 
-
-Lemma ZplusrN : right_inverse 0%Z Z.opp Zplus.
-Proof. exact Zplus_opp_r. Qed.
-
-HB.instance Definition _ := @GRing.isZmodule.Build Z _ _ _ ZplusA ZplusC Zplus0 ZplusNr.
-
-(* Z Ring *)
-Lemma ZmultA : associative Zmult.
-Proof. exact: Zmult_assoc. Qed.
-
-Lemma Zmult1q : left_id 1%Z Zmult.
-Proof. exact: Zmult_1_l. Qed.
-
-Lemma Zmultq1 : right_id 1%Z Zmult.
-Proof. exact: Zmult_1_r. Qed.
-
-Lemma Zmultq0 : forall (q : Z), Zmult q 0%Z = 0%Z.
-Proof. exact: Zmult_0_r. Qed.
-
-Lemma Zmult_addl : left_distributive Zmult Zplus.
-Proof. exact: Zmult_plus_distr_l. Qed.
-
-Lemma Zmult_addr : right_distributive Zmult Zplus.
-Proof. exact: Zmult_plus_distr_r. Qed.
-
-Lemma nonzeroZ1 : 1%Z != 0%Z.
-Proof. by []. Qed.
-
-HB.instance Definition _ := @GRing.Zmodule_isRing.Build Z _ _ ZmultA Zmult1q Zmultq1 Zmult_addl Zmult_addr nonzeroZ1.
-
-Lemma ZmultC : commutative Zmult.
-Proof. exact: Zmult_comm. Qed.
-
-HB.instance Definition _ := @GRing.Ring_hasCommutativeMul.Build Z ZmultC.
-
-(* Warning : an antisymmetric an a transitive predicates are
-present in loaded Relations.Relation_Definition *)
-Lemma Zle_bool_antisymb : ssrbool.antisymmetric  Zle_bool.
-Proof. by move=> x y; case/andP=> h1 h2; apply: Zle_bool_antisym. Qed.
-
-Lemma Zle_bool_transb : ssrbool.transitive Zle_bool.
-Proof. move=> x y z; exact: Zle_bool_trans. Qed.
-
-Lemma Zle_bool_totalb : total Zle_bool.
-Proof. by move=> x y; case: (Zle_bool_total x y)=> -> //; rewrite orbT. Qed.
-
-Lemma Zle_bool_addr : forall z x y, Zle_bool x y -> Zle_bool (x + z) (y + z).
-Proof. by move=> x y z h; rewrite Zle_bool_plus_mono // Zle_bool_refl. Qed.
-
-Lemma Zle_bool_mulr : forall x y, 
-  Zle_bool 0 x -> Zle_bool 0 y -> Zle_bool 0 (x * y).
-Proof. 
-move=> x y; move/Zle_is_le_bool=> px; move/Zle_is_le_bool=> py.
-by apply/Zle_is_le_bool; apply: Zmult_le_0_compat.
-Qed.
-
-Definition Zunit := pred2 1%Z (-1)%Z.
-
-Definition Zinv (z : Z) := z.
-
-
-Lemma ZmulV : {in Zunit, left_inverse 1%R Zinv *%R}.
-Proof. by move=> x; rewrite inE; case/pred2P => ->. Qed.
-
-(* Zmult_1_inversion_r does not exist *)
-Lemma unitZPl : forall x y, y * x = 1 -> Zunit x.
-Proof.
-move=> x y; rewrite mulrC.
-rewrite -[x * y]/(Zmult x y); move/Zmult_1_inversion_l.
-by case=> ->.
-Qed.
-
-Lemma  Zinv_out : {in predC Zunit, Zinv =1 id}.
-Proof. exact. Qed.
-
-HB.instance Definition _ := GRing.ComRing_hasMulInverse.Build Z ZmulV unitZPl Zinv_out.
-
-Lemma Z_idomain_axiom : forall x y : Z,
-  x * y = 0 -> (x == 0) || (y == 0).
-Proof.
-move=> x y; rewrite -[x * y]/(Zmult x y); move/Zmult_integral; case=> -> //=.
-by rewrite eqxx orbT.
-Qed.
-
-HB.instance Definition _ := @GRing.ComUnitRing_isIntegral.Build Z Z_idomain_axiom.
-
-Lemma Zlt_def (x y : Z) : (x <? y)%Z = (y != x) && (x <=? y)%Z.
-Proof.
-(* TODO *)
-Admitted.
-
-Lemma Zle_total : forall m n : Z, (m <=? n)%Z || (n <=? m)%Z.
-Proof.
-(* TODO *)
-Admitted.
-
-(*Definition Z_OrderedRingMixin :=
-  OrderedRing.Mixin 
-  Zle_bool_antisymb Zle_bool_transb Zle_bool_totalb Zle_bool_addr Zle_bool_mulr.*)
-Lemma Z_display : Datatypes.unit. Proof. exact: tt. Qed.
-(*Definition Z_OrderedRingMixin :=
-  @LePOrderMixin Z_eqType Z.leb Z.ltb Zlt_def Zle_bool_refl Zle_bool_antisymb Zle_bool_transb.
-Canonical Z_porderType := POrderType Z_display Z Z_OrderedRingMixin.*)
-
-HB.instance Definition _ :=
-  @Order.isOrder.Build Z_display Z _ _ _ _ Zlt_def (fun _ _ => erefl) (fun _ _ => erefl) Zle_bool_antisymb Zle_bool_transb Zle_total.
-
-(*Canonical Structure Z_OrderedRingType :=
-  Eval hnf in OIdomainType Z Z_OrderedRingMixin.
-
-Canonical Structure Z_oIdomainType :=
-  Eval hnf in OIdomainType Z Z_OrderedRingMixin.*)
-
-(* Basic tructures for rational numbers.*)
-
-(* TODO
-
-Definition eqq (x y : Q) : bool :=
-  match x, y with
-    | (xn # xd)%Q, (yn # yd)%Q => (xn == yn) && (xd == yd)
-  end.
-
-Lemma eqq_refl : forall q, eqq q q.
-Proof. by move=> [d n]; rewrite /eqq; rewrite 2!eqxx. Qed.
-
-Lemma eqqP : Equality.axiom eqq.
-Proof.
-  move=> q1 q2; apply: (iffP idP) => [|<-]; last exact: eqq_refl.
-  by case: q1=> n1 d1; case: q2=> n2 d2; case/andP; move/eqP->; move/eqP->.
-Qed.
-
-Canonical Structure eqq_eqMixin := EqMixin eqqP.
-Canonical Structure eqq_eqType := Eval hnf in EqType Q eqq_eqMixin.
-
-Definition q_code (q : Q) :=
-  match q with
-    |(qnum # qden)%Q => (qnum, qden)
-  end.
-
-Definition q_pickle q := pickle (q_code q).
-
-Definition q_decode c :=
-  match c with
-    |(q, d) => Some (q # d)%Q
-  end.
-
-Definition q_unpickle n :=
-  match (unpickle n) with
-    |None => None
-    |Some u => q_decode u
-  end.
-
-Lemma q_codeK : pcancel q_code q_decode.
-Proof. by move=> []. Qed.
-
-Lemma q_pick_cancel : pcancel q_pickle q_unpickle.
-Proof.
-by move=> x; rewrite /q_pickle /q_unpickle pickleK q_codeK.
-Qed.
-
-Definition q_countMixin  := CountMixin q_pick_cancel.
-Definition q_choiceMixin := CountChoiceMixin q_countMixin.
-
-Canonical Structure q_choiceType :=
-  Eval hnf in ChoiceType  Q q_choiceMixin.
-Canonical Structure q_countType :=
-  Eval hnf in CountType Q q_countMixin.
-
-(*
-Definition nnegqb (q : Q) :=
-  match q with
-    (qd # qn)%Q => match qd with Zneg _ => false | _ => true end
-  end.
-*)
-
-
-(* Basic and algebraic structures for normalized rational numbers,
-we do not intend to be specially clever wrt normalization at this point *)
-
-Record Qcb : Type := QcbMake { qcb_val :> Q; _ : Qred qcb_val == qcb_val }.
-
-Canonical Structure qcb_subType :=
-  Eval hnf in [subType for qcb_val by Qcb_rect].
-
-Definition qcb_eqMixin := Eval hnf in [eqMixin of qcb_subType by <:].
-Canonical Structure qcb_eqType  := Eval hnf in EqType Qcb qcb_eqMixin.
-
-Definition qcb_choiceMixin := [choiceMixin of Qcb by <:].
-Canonical Structure qcb_choiceType :=
-  Eval hnf in ChoiceType Qcb  qcb_choiceMixin.
-
-Definition qcb_countMixin := [countMixin of Qcb by <:].
-Canonical Structure qcb_countType :=
-  Eval hnf in CountType Qcb qcb_countMixin.
-
-Canonical Structure qcb_subCountType :=
-  Eval hnf in [subCountType of Qcb].
-
-(* Properties about Qred, Q and Qcb and equalities over all these types *)
-Lemma Qredb_involutive : forall q, Qred (Qred q) == (Qred q).
-Proof. by move=> q; apply/eqP; apply Qred_involutive. Qed.
-
-(*
-Lemma Qcb_is_canon : forall (q q' : Qcb), (q == q')%Q -> q = q'.
-Proof.
-move=> [x hx] [y hy]; move/Qred_complete=> /=; rewrite (eqP hx) (eqP hy)=> e.
-by apply:val_inj.
-Qed.
-*)
-
-Lemma Qredb_complete : forall q q', (q == q')%Q -> Qred q == Qred q'.
-Proof. by move=> q q' H; apply/eqP; apply Qred_complete. Qed.
-
-Lemma Qcb_QeqP : forall (q q': Qcb), reflect (q == q')%Q (q == q').
-Proof.
-move=> [q Hq] [q' Hq']; apply: (iffP eqP)=> [|]; first by move->.
-by move/Qred_complete=> H; apply: val_inj=> /=; rewrite -(eqP Hq) -(eqP Hq').
-Qed.
-
-Lemma Qcb_is_canon : forall (q q' : Qcb), (q == q')%Q -> q == q'.
-Proof.
-  case=> q Hq; case=> q' Hq'; rewrite eqE /= => H.
-  by rewrite -(eqP Hq) -(eqP Hq'); apply Qredb_complete.
-Qed.
-
-(* Arithmetic over Qcb from the one over Q *)
-Definition Q2Qcb (q:Q) : Qcb := QcbMake (Qredb_involutive q).
-Arguments Scope Q2Qc [Q_scope].
-
-Definition Qcbplus  (x y : Qcb) := Q2Qcb (x + y).
-Definition Qcbmult  (x y : Qcb) := Q2Qcb (x * y).
-Definition Qcbopp   (x   : Qcb) := Q2Qcb (- x).
-Definition Qcbminus (x y : Qcb) := Q2Qcb (x - y).
-Definition Qcbinv   (x   : Qcb) := Q2Qcb (/x).
-Definition Qcbdiv   (x y : Qcb) := Q2Qcb (x */ y).
-
-(* just for the tactic *)
-Lemma qcb_valE : forall x Hx, qcb_val (@QcbMake x Hx) = x .
-Proof . by [] . Qed .
-
-Tactic Notation "qcb" tactic(T) :=
-    repeat case=> ? ?;
-      apply/eqP; apply Qcb_is_canon;
-      rewrite !qcb_valE; repeat setoid_rewrite Qred_correct;
-      by T.
-
-
-Lemma QcbplusA : associative Qcbplus.
-Proof.
-case=> [x hx] [y hy] [z hz]; apply: val_inj; apply: Qred_complete.
-rewrite /= -/(Qred (Qplus y z)) -/(Qred (Qplus x y)).
-repeat setoid_rewrite Qred_correct; ring.
-Qed.
-
-
-Lemma QcbplusC : commutative Qcbplus.
-Proof.
-case=> [x hx] [y hy]; apply: val_inj; apply: Qred_complete.
-by rewrite Qplus_comm.
-Qed.
-
-Lemma Qcbplus0q : left_id (Q2Qcb 0) Qcbplus.
-case=> [x hx];  apply: val_inj; rewrite /= -/(Qred (Qplus 0 x)).
-rewrite -{2}(eqP hx). apply: Qred_complete.
-by rewrite Qplus_0_l.
-Qed.
-
-Lemma QcbplusNq : left_inverse (Q2Qcb 0) Qcbopp Qcbplus.
-Proof. by qcb ring. Qed.
-
-Lemma QcbplusqN : right_inverse (Q2Qcb 0) Qcbopp Qcbplus.
-Proof. by qcb ring. Qed.
-
-Definition Qcb_zmodMixin :=
-  ZmodMixin QcbplusA QcbplusC Qcbplus0q QcbplusNq.
-
-
-Canonical Structure Qcb_zmodType :=
-  Eval hnf in ZmodType Qcb Qcb_zmodMixin.
-
-(* Q/== ==> Ring *)
-Lemma QcbmultA : associative Qcbmult.
-Proof. by qcb ring. Qed.
-
-Lemma Qcbmult1q : left_id (Q2Qcb 1) Qcbmult.
-Proof. by qcb ring. Qed.
-
-Lemma Qcbmultq1 : right_id (Q2Qcb 1) Qcbmult.
-Proof. by qcb ring. Qed.
-
-Lemma Qcbmultq0 : forall (q : Qcb), Qcbmult q (Q2Qcb 0) = (Q2Qcb 0).
-Proof. by qcb ring. Qed.
-
-Lemma Qcbmult_addl : left_distributive Qcbmult Qcbplus.
-Proof. by qcb ring. Qed.
-
-Lemma Qcbmult_addr : right_distributive Qcbmult Qcbplus.
-Proof. by qcb ring. Qed.
-
-Lemma nonzeroq1 : Q2Qcb 1 != Q2Qcb 0.
-Proof. by rewrite /Q2Qcb eqE /=. Qed.
-
-Definition Qcb_ringMixin :=
-  RingMixin QcbmultA Qcbmult1q Qcbmultq1 Qcbmult_addl Qcbmult_addr nonzeroq1.
-Canonical Structure Qcb_ringType :=
-  Eval hnf in RingType Qcb Qcb_ringMixin.
-
-(* Q/== ==> commutative ring *)
-Lemma QcbmultC : commutative Qcbmult.
-Proof. by qcb ring. Qed.
-
-Canonical Structure Qcb_comRingType := ComRingType Qcb QcbmultC.
-
-(* Q/== ==> ring with units *)
-Lemma Qcb_mulVx :
-    forall x:Qcb, x != (Q2Qcb 0) -> Qcbmult (Qcbinv x) x = (Q2Qcb 1).
-Proof.
-  case=> x Hx; move=> H; apply/eqP; apply Qcb_is_canon.
-  rewrite QcbmultC !qcb_valE; repeat setoid_rewrite Qred_correct.
-  by apply Qmult_inv_r => Hx0; case/Qcb_QeqP: H.
-Qed.
-
-Lemma Qcb_mulxV :
-    forall x:Qcb, x != (Q2Qcb 0) -> Qcbmult x (Qcbinv x) = (Q2Qcb 1).
-Proof.
-  by move=> x Hx; rewrite QcbmultC; apply Qcb_mulVx.
-Qed.
-
-Definition Qcb_unit : pred Qcb := fun q:Qcb => q != (Q2Qcb 0).
-
-Lemma Qcb_intro_unit :
-    forall (p q : Qcb), Qcbmult q p = (Q2Qcb 1) -> p != (Q2Qcb 0).
-Proof.
-  move=> p q H; apply/negP; move/eqP => p0.
-  by rewrite p0 Qcbmultq0 in H.
-Qed.
-
-Lemma Qcb_intro_unit_nC :
-    forall (p q : Qcb),
-      Qcbmult q p = (Q2Qcb 1) /\ Qcbmult p q = (Q2Qcb 1)
-      -> p != (Q2Qcb 0).
-Proof.
-  by move=> p q *; apply (@Qcb_intro_unit p q); tauto.
-Qed.
-
-Lemma Qcb_inv_out : forall (p : Qcb), negb (p != (Q2Qcb 0)) -> Qcbinv p = p.
-Proof.
-  by move=> p H; rewrite negbK in H; rewrite (eqP H) /Qcbinv /= /Qinv.
-Qed.
-
-(* FIXME strub: cannot do 1/x when defining Qcb_unitRingType as:
-
-   Canonical Structure Qcb_unitRingType :=
-      Eval hnf in UnitRingType Qcb_comUitRingMixin. *)
-
-Definition Qcb_unitRingMixin :=
-  UnitRingMixin Qcb_mulVx Qcb_mulxV Qcb_intro_unit_nC Qcb_inv_out.
-
-Definition Qcb_comUnitRingMixin :=
-  ComUnitRingMixin Qcb_mulVx Qcb_intro_unit Qcb_inv_out.
-
-Canonical Structure Qcb_unitRingType :=
-   Eval hnf in UnitRingType Qcb Qcb_unitRingMixin.
-
-Canonical Structure Qcb_comUnitRingType := [comUnitRingType of Qcb].
-
-(* Q/== ==> field *)
-Definition Qcb_fieldMixin : GRing.Field.mixin_of Qcb_comUnitRingType.
-Proof. by []. Qed.
-
-Definition Qcb_idomainMixin := FieldIdomainMixin Qcb_fieldMixin.
-
-Canonical Structure Qcb_iddomainType :=
-  Eval hnf in IdomainType Qcb Qcb_idomainMixin.
-
-Canonical Structure Qcb_fieldType :=
-  Eval hnf in FieldType Qcb Qcb_fieldMixin.
-
-(*
-Definition Qcb_leb  (x y : Q) := 
-  (Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
-Definition Qcb_ltb  (x y : Q) := 
-  (Zlt_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
-*)
-(*
-Local Notation "x <<= y" := (Qcb_leb x y).
-Local Notation "x <<! y" := (Qcb_ltb x y).
-*)
-
-Definition Qcbleb (x y : Qcb) := (Qle_bool x y).
-
-Lemma QcblebP : forall (x y : Qcb), reflect (x <= y)%Q (Qcbleb x y).
-Proof. by move=> x y; apply: (iffP idP); move/Qle_bool_iff. Qed.
-
-Lemma Qcbleb_antisymb : @ssrbool.antisymmetric Qcb Qcbleb.
-Proof. 
-move=> x y; case/andP; move/QcblebP=> h1; move/QcblebP=> h2.
-by apply/eqP; apply/Qcb_QeqP; apply: Qle_antisym.
-Qed.
-
-Lemma Qcbleb_transb : @ssrbool.transitive Qcb Qcbleb.
-Proof. 
-move=> x y z; move/QcblebP=> h1; move/QcblebP=> h2; apply/QcblebP. 
-exact: Qle_trans h2.
-Qed.
-
-Lemma Qcbleb_totalb : @ssrbool.total Qcb Qcbleb.
-Proof.
-move=> x y; case e: (Qcbleb x y)=> //=.
-by move/QcblebP: e; move/Qnot_le_lt; move/Qlt_le_weak; move/QcblebP->.
-Qed.
-
-Lemma Qcbleb_addr : forall z x y : Qcb, 
-  Qcbleb x y -> Qcbleb (x + z) (y + z).
-Proof. 
-move=> [x Hx] [y Hy] [z Hz]; move/QcblebP => Hxy; apply/QcblebP.
-rewrite !qcb_valE in Hxy *.
-setoid_rewrite Qred_correct.
-by apply Qplus_le_compat; last apply Qle_refl .
-Qed.
-
-Lemma Qle_bool_mulr : forall x y, 
-  Qle_bool 0 x -> Qle_bool 0 y -> Qle_bool 0 (x * y).
-Proof. 
-move=> x y; move/Zle_is_le_bool; rewrite Zmult_1_r=> px.
-move/Zle_is_le_bool; rewrite Zmult_1_r => py.
-by apply/Zle_is_le_bool; rewrite Zmult_1_r; apply: Zmult_le_0_compat.
-Qed.
-
-Lemma Qcbleb_mulr : forall x y, Qcbleb 0 x -> Qcbleb 0 y -> Qcbleb 0 (x * y).
-Proof.
-  move=> x y; move/QcblebP; rewrite qcb_valE; setoid_rewrite Qred_correct=> hx.
-  move/QcblebP; rewrite qcb_valE; setoid_rewrite Qred_correct=> hy.
-  apply/QcblebP; rewrite !qcb_valE; setoid_rewrite Qred_correct.
-  exact: Qmult_le_0_compat.
-Qed.
-
-Definition Q_OrderedRingMixin := 
-  OrderedRing.Mixin 
-  Qcbleb_antisymb Qcbleb_transb Qcbleb_totalb Qcbleb_addr Qcbleb_mulr.
-
-Canonical Structure Qcb_oIddomainType :=
-  Eval hnf in OIdomainType Qcb Q_OrderedRingMixin.
-
-Canonical Structure Qcb_oFieldType :=
-  Eval hnf in OFieldType Qcb Q_OrderedRingMixin.
-
-*)
diff --git a/theories/intersection.v b/theories/intersection.v
index 74335e7..ea9d5b0 100644
--- a/theories/intersection.v
+++ b/theories/intersection.v
@@ -1,5 +1,7 @@
 Require Export counterclockwise conv encompass preliminaries.
-From mathcomp Require Import all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets constructive_ereal.
+From mathcomp Require Import all_ssreflect ssralg matrix ssrnum vector reals.
+From mathcomp Require Import normedtype order boolp classical_sets.
+From mathcomp Require Import constructive_ereal.
 
 (******************************************************************************)
 (*  separated a b c d == true if a = b or (ab) intersects [c,d]               *)
@@ -204,8 +206,6 @@ Qed.
    show that b <| t |> a is between x and y, which concludes the proof.
    *)
 
-Import Order.TBLatticeTheory.
-
 Lemma hull_border_no_intersection (l : seq Plane) (a b : Plane) :
   (3 <= size l)%N ->
   uniq l ->
@@ -307,7 +307,7 @@ have : [exists i : 'I_(size l), det l`_i l`_i.+1mod (b <| sup I |> a) <= 0].
   have t01: in01 (fine (mine t 1%E)).
     apply/andP; split; rewrite -lee_fin tfin; last by rewrite lteIx le_refl orbT.
     rewrite ltexI; apply/andP; split; last by rewrite lee_fin ler01.
-    apply: Order.TLatticeTheory.meets_ge => i abgt; rewrite lee_fin; apply: (mulr_ge0 (la _)).
+    apply: Order.TMeetTheory.meets_ge => i abgt; rewrite lee_fin; apply: (mulr_ge0 (la _)).
     by apply ltW; rewrite invr_gt0 -2![det l`_i _ _]det_cyclique.
   apply: sup_upper_bound => //; apply/andP; split => //.
   rewrite encompass_all_index l0/=; apply/forallP => i.
@@ -318,7 +318,7 @@ have : [exists i : 'I_(size l), det l`_i l`_i.+1mod (b <| sup I |> a) <= 0].
     rewrite -subr_ge0 -(pmulr_lge0 _ abgt0) mulrBl subr_ge0 -mulrA divff// mulr1.
     rewrite -lee_fin tfin leIx; apply/orP; left.
     rewrite ![det _ l`_i _]det_cyclique /t.
-    by move:abgt0; rewrite invr_gt0=>abgt; exact: Order.TLatticeTheory.meets_inf.
+    by move:abgt0; rewrite invr_gt0=>abgt; exact: Order.TMeetTheory.meets_inf.
   rewrite {2}[det a _ _]det_cyclique (le_trans _ (la i))// mulr_ge0_le0 //.
   by move:t01 => /andP[].
 move=> /existsP[i] iable0.
diff --git a/theories/preliminaries.v b/theories/preliminaries.v
index 1d0f456..a2ff380 100644
--- a/theories/preliminaries.v
+++ b/theories/preliminaries.v
@@ -14,11 +14,9 @@ Elpi Query lp:{{
   coq.say "snd primproj" Q2 N2
 }}.
 
-
-
-Require Import Reals.
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra vector reals classical_sets Rstruct.
+From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import classical_sets reals Rstruct.
 From infotheo Require Import convex.
 
 Import GRing.Theory Num.Theory convex.
@@ -29,7 +27,6 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 (* TODO: move to mathcomp ? *)
-
 Lemma enum_rank_index {T : finType} i :
   nat_of_ord (enum_rank i) = index i (enum T).
 Proof.
@@ -162,7 +159,9 @@ case: i; case=>[| i] ilt.
 by left; exists (Ordinal (ltnSE ilt)); apply val_inj.
 Qed.
 
-Lemma subseq_incl (T: eqType) (s s': seq T) x: subseq s s' -> {f: 'I_(size s) -> 'I_(size s') | (forall i, nth x s' (f i) = nth x s i) /\ {homo f : y x / (x < y)%O >-> (x < y)%O}}.
+Lemma subseq_incl (T : eqType) (s s' : seq T) x : subseq s s' ->
+  {f : 'I_(size s) -> 'I_(size s') | (forall i, nth x s' (f i) = nth x s i) /\
+    {homo f : y x / (x < y)%O >-> (x < y)%O}}.
 Proof.
 elim: s' s=> [| a s' IHs'] s sub.
    by move:sub=>/eqP -> /=; exists id; split=>// i j.
@@ -181,7 +180,7 @@ move: sub=>/=; case sa: (b == a).
 by move=>/IHs' [f [fn flt]]; exists (fun i => lift ord0 (f i)).
 Qed.
 
-Lemma hom_lt_inj {disp disp' : unit} {T : orderType disp} {T' : porderType disp'} [f : T -> T'] :
+Lemma hom_lt_inj {disp disp'} {T : orderType disp} {T' : porderType disp'} [f : T -> T'] :
   {homo f : x y / (x < y)%O >-> (x < y)%O} -> injective f.
 Proof.
 move=>flt i j.
@@ -215,8 +214,8 @@ case Pa: (P a).
 by case: n=>//=; rewrite ltnS; apply IHs.
 Qed.
 
-Lemma big_pair [R : Type] (idr : R) (opr : R -> R -> R) [S : Type] (ids : S) (ops : S -> S -> S) [I : Type]
-  (r : seq I) (F : I -> R) (G: I -> S) :
+Lemma big_pair [R : Type] (idr : R) (opr : R -> R -> R) [S : Type] (ids : S)
+    (ops : S -> S -> S) [I : Type] (r : seq I) (F : I -> R) (G: I -> S) :
   \big[(fun (x y: R*S)=> (opr x.1 y.1, ops x.2 y.2))/(idr, ids)]_(i <- r) (F i, G i) =
   (\big[opr/idr]_(i <- r) F i, \big[ops/ids]_(i <- r) G i).
 Proof.
@@ -228,12 +227,15 @@ Qed.
 From infotheo Require Import fdist.
 Local Open Scope fdist_scope.
 
-Lemma Convn_pair [T U : convType] [n : nat] (g : 'I_n -> T * U) (d : {fdist 'I_n}) :
-  Convn conv d g = (Convn conv d (Datatypes.fst \o g), Convn conv d (Datatypes.snd \o g)).
+Lemma Convn_pair [T U : @convType Rdefinitions.R] [n : nat] (g : 'I_n -> T * U)
+    (d : {fdist 'I_n}) :
+  Convn conv d g = (Convn conv d (Datatypes.fst \o g),
+                    Convn conv d (Datatypes.snd \o g)).
 Proof.
 elim: n g d => [|n IHn] g d.
    by have := fdistI0_False d.
-rewrite /Convn; case: (Bool.bool_dec _ _) => [_|d0]; first by rewrite -surjective_pairing.
+rewrite /Convn; case: (Bool.bool_dec _ _) => [_|d0].
+  by rewrite -surjective_pairing.
 have := IHn (g \o fdist_del_idx ord0) (fdist_del (Bool.eq_true_not_negb _ d0)).
 by rewrite/Convn => ->.
 Qed.
diff --git a/theories/preliminaries_hull.v b/theories/preliminaries_hull.v
index 667a501..496b471 100644
--- a/theories/preliminaries_hull.v
+++ b/theories/preliminaries_hull.v
@@ -116,7 +116,7 @@ case: (ord_S_split a).
 by move=>_; rewrite inE.
 Qed.
 
-Lemma homo_lt_total {disp disp' : unit} {T : orderType disp}
+Lemma homo_lt_total disp disp' {T : orderType disp}
    {T' : orderType disp'} [f : T -> T'] : {homo f : x y / x < y >-> x < y} ->
    forall x y, f x < f y -> x < y.
 Proof.
@@ -126,7 +126,7 @@ move:xy=>/negbT/lt_total/orP; case=>// /fh fyx.
 by move:(lt_trans fxy fyx); rewrite lt_irreflexive.
 Qed.
 
-Lemma homo_lt_inj {disp disp' : unit} {T : orderType disp}
+Lemma homo_lt_inj {disp disp'} {T : orderType disp}
    {T' : orderType disp'} [f : T -> T'] : {homo f : x y / x < y >-> x < y} ->
    injective f.
 Proof.
diff --git a/theories/safe_cells.v b/theories/safe_cells.v
index b689cd1..45e352e 100644
--- a/theories/safe_cells.v
+++ b/theories/safe_cells.v
@@ -17,14 +17,14 @@ Section safety_property.
 
 Variable R : realFieldType.
 
-Notation pt := (@pt (RealField.sort R)).
+Notation pt := (@pt (Num.RealField.sort R)).
 Notation p_x := (p_x R).
 Notation p_y := (p_y R).
 Notation Bpt := (Bpt R).
 Notation edge := (@edge R).
-Notation cell := (@cell (RealField.sort R) edge).
-Notation low := (low (RealField.sort R) edge).
-Notation high := (high (RealField.sort R) edge).
+Notation cell := (@cell (Num.RealField.sort R) edge).
+Notation low := (low (Num.RealField.sort R) edge).
+Notation high := (high (Num.RealField.sort R) edge).
 Notation left_pts := (left_pts R edge).
 Notation right_pts := (right_pts R edge).
 Notation dummy_pt := (dummy_pt R 1).
@@ -32,19 +32,19 @@ Notation event := (@event R edge).
 Notation point' := (@point R edge).
 Notation outgoing := (@point R edge).
 Notation point_under_edge :=
-  (point_under_edge (RealField.sort R) <=%R +%R (fun x y => x - y)
+  (point_under_edge (Num.RealField.sort R) <=%R +%R (fun x y => x - y)
     *%R 1 edge (@left_pt R)(@right_pt R)).
 Notation "p <<= e" := (point_under_edge p e).
 Notation "p >>> e" := (negb (point_under_edge p e)).
 Notation valid_edge :=
-  (valid_edge (RealField.sort R) <=%R edge (@left_pt R) (@right_pt R)).
+  (valid_edge (Num.RealField.sort R) <=%R edge (@left_pt R) (@right_pt R)).
 Notation point_strictly_under_edge :=
-  (point_strictly_under_edge (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (point_strictly_under_edge (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
     *%R 1 edge (@left_pt R)(@right_pt R)).
 Notation "p <<< e" := (point_strictly_under_edge p e).
 Notation "p >>= e" := (negb (point_strictly_under_edge p e)).
 Notation edge_below :=
-  (generic_trajectories.edge_below (RealField.sort R) eq_op <=%R +%R
+  (generic_trajectories.edge_below (Num.RealField.sort R) eq_op <=%R +%R
     (fun x y => x - y) *%R 1 edge (@left_pt R) (@right_pt R)).
 Notation "x <| y" := (edge_below x y).
 
@@ -262,46 +262,46 @@ Section main_statement.
 
 Variable R : realFieldType.
 
-Notation pt := (@pt (RealField.sort R)).
-Notation p_x := (p_x (RealField.sort R)).
-Notation p_y := (p_y (RealField.sort R)).
-Notation Bpt := (Bpt (RealField.sort R)).
+Notation pt := (@pt (Num.RealField.sort R)).
+Notation p_x := (p_x (Num.RealField.sort R)).
+Notation p_y := (p_y (Num.RealField.sort R)).
+Notation Bpt := (Bpt (Num.RealField.sort R)).
 Notation edge := (@edge R).
-Notation cell := (@cell (RealField.sort R) edge).
-Notation low := (low (RealField.sort R) edge).
-Notation high := (high (RealField.sort R) edge).
-Notation left_pts := (left_pts (RealField.sort R) edge).
-Notation right_pts := (right_pts (RealField.sort R) edge).
-Notation dummy_pt := (dummy_pt (RealField.sort R) 1).
-Notation event := (@event (RealField.sort R) edge).
-Notation point := (@point (RealField.sort R) edge).
-Notation outgoing := (@outgoing (RealField.sort R) edge).
+Notation cell := (@cell (Num.RealField.sort R) edge).
+Notation low := (low (Num.RealField.sort R) edge).
+Notation high := (high (Num.RealField.sort R) edge).
+Notation left_pts := (left_pts (Num.RealField.sort R) edge).
+Notation right_pts := (right_pts (Num.RealField.sort R) edge).
+Notation dummy_pt := (dummy_pt (Num.RealField.sort R) 1).
+Notation event := (@event (Num.RealField.sort R) edge).
+Notation point := (@point (Num.RealField.sort R) edge).
+Notation outgoing := (@outgoing (Num.RealField.sort R) edge).
 Notation point_under_edge :=
-  (point_under_edge (RealField.sort R) <=%R +%R (fun x y => x - y)
+  (point_under_edge (Num.RealField.sort R) <=%R +%R (fun x y => x - y)
     *%R 1 edge (@left_pt R)(@right_pt R)).
 Notation "p <<= e" := (point_under_edge p e).
 Notation "p >>> e" := (negb (point_under_edge p e)).
 Notation valid_edge :=
-  (valid_edge (RealField.sort R) <=%R edge (@left_pt R) (@right_pt R)).
+  (valid_edge (Num.RealField.sort R) <=%R edge (@left_pt R) (@right_pt R)).
 Notation point_strictly_under_edge :=
-  (point_strictly_under_edge (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (point_strictly_under_edge (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
     *%R 1 edge (@left_pt R)(@right_pt R)).
 Notation "p <<< e" := (point_strictly_under_edge p e).
 Notation "p >>= e" := (negb (point_strictly_under_edge p e)).
 Notation edge_below :=
-  (generic_trajectories.edge_below (RealField.sort R) eq_op <=%R +%R
+  (generic_trajectories.edge_below (Num.RealField.sort R) eq_op <=%R +%R
     (fun x y => x - y) *%R 1 edge (@left_pt R) (@right_pt R)).
 Notation "x <| y" := (edge_below x y).
 
 Notation vertical_intersection_point :=
-  (vertical_intersection_point (RealField.sort R) le +%R
+  (vertical_intersection_point (Num.RealField.sort R) <=%R +%R
   (fun x y => x - y) *%R
   (fun x y => x / y) edge (@left_pt R) (@right_pt R)).
 Notation leftmost_points :=
- (leftmost_points (RealField.sort R) eq_op le +%R (fun x y => x - y) *%R
+ (leftmost_points (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R
   (fun x y => x / y) edge (@left_pt R) (@right_pt R)).
 Notation start_open_cell :=
-  (start_open_cell (RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R
+  (start_open_cell (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R
   (fun x y => x / y) edge (@left_pt R) (@right_pt R)).
 
 Arguments pt_eqb : simpl never.