diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index c02ae96b06709a1340090c908b3d05af0bbad0ff..790c414deadd8ec25dcfd42b31ba59f5ae2e3045 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -39,31 +39,29 @@ End Bool_compl.
 Section Seq_compl1.
 
 Context {T : Type}.
+Context {x0 x : T}.
+Context {l : seq T}.
+Context {i : nat}.
 
-Lemma nth_cons_l : forall {x0 x : T} {l i}, i = 0 -> nth x0 (x :: l) i = x.
+Lemma nth_cons_l : i = 0 -> nth x0 (x :: l) i = x.
 Proof. intros; subst; apply nth0. Qed.
 
-Lemma nth_cons_r :
-  forall {x0 x : T} {l i}, i <> 0 -> nth x0 (x :: l) i = nth x0 l (i - 1).
+Lemma nth_cons_r : i <> 0 -> nth x0 (x :: l) i = nth x0 l (i - 1).
 Proof.
-intros x0 x l i Hi; rewrite (nth_ncons _ 1); case_eq (i < 1); try easy.
+intros Hi; rewrite (nth_ncons _ 1); case_eq (i < 1); try easy.
 move=> /ltP Hi1; contradict Hi; apply lt_1; easy.
 Qed.
 
-Lemma nth_rcons_l :
-  forall {x0 x : T} {l i}, i <> size l -> nth x0 (rcons l x) i = nth x0 l i.
+Lemma nth_rcons_l : i <> size l -> nth x0 (rcons l x) i = nth x0 l i.
 Proof.
-intros x0 x l i Hi; rewrite nth_rcons;
-    case_eq (i < size l); intros Hi1; try easy.
+intros Hi; rewrite nth_rcons; case_eq (i < size l); intros Hi1; try easy.
 case_eq (i == size l); intros Hi2; try now contradict Hi; apply /eqP.
 symmetry; apply nth_default; rewrite leqNgt Hi1; easy.
 Qed.
 
-Lemma nth_rcons_r :
-  forall {x0 x : T} {l i}, i = size l -> nth x0 (rcons l x) i = x.
+Lemma nth_rcons_r : i = size l -> nth x0 (rcons l x) i = x.
 Proof.
-intros x0 x l i Hi; subst; rewrite nth_rcons;
-    case_eq (size l < size l); intros Hl1.
+intros Hi; subst; rewrite nth_rcons; case_eq (size l < size l); intros Hl1.
 exfalso; rewrite ltnn in Hl1; easy.
 case_eq (size l == size l); intros Hl2; try easy.
 exfalso; rewrite eq_refl in Hl2; easy.
@@ -75,12 +73,14 @@ End Seq_compl1.
 Section Seq_compl2.
 
 Context {T : eqType}.
+Context {x0 x : T}.
+Context {l : seq T}.
+Context {i : nat}.
 
 Lemma nth_cons_l_rev :
-  forall {x0 x : T} {l : seq T} {i},
-    x \notin l -> i <= size l -> nth x0 (x :: l) i = x -> i = 0.
+  x \notin l -> i <= size l -> nth x0 (x :: l) i = x -> i = 0.
 Proof.
-intros x0 x l i Hx Hi H; destruct l as [| y l].
+intros Hx Hi H; destruct l.
 apply /eqP; rewrite leqn0 // in Hi.
 destruct (le_dec i 0) as [Hi0 | Hi0]; auto with arith.
 apply Nat.nle_gt in Hi0; move: Hi0 => /ltP Hi0.
@@ -91,33 +91,37 @@ clear x H; apply mem_nth; rewrite ltn_psubLR //.
 Qed.
 
 Lemma nth_cons_l_rev_uniq :
-  forall {x0 x} {l : seq T} {i},
-    uniq (x :: l) -> i <= size l -> nth x0 (x :: l) i = x -> i = 0.
+  uniq (x :: l) -> i <= size l -> nth x0 (x :: l) i = x -> i = 0.
 Proof. move=>> /andP [Hx _]; apply nth_cons_l_rev; easy. Qed.
 
 Lemma nth_rcons_r_rev :
-  forall {x0 x : T} {l : seq T} {i},
-    x \notin l -> i <= size l -> nth x0 (rcons l x) i = x -> i = size l.
+  x \notin l -> i <= size l -> nth x0 (rcons l x) i = x -> i = size l.
 Proof.
-intros x0 x l i Hx Hi H; destruct (lastP l) as [| l y].
+intros Hx Hi H; destruct (lastP l) as [| s y].
 apply /eqP; rewrite leqn0 // in Hi.
-destruct (le_dec (size (rcons l y)) i) as [Hi1 | Hi1].
+destruct (le_dec (size (rcons s y)) i) as [Hi1 | Hi1].
 apply Nat.le_antisymm; try easy; apply /leP; easy.
 apply Nat.nle_gt in Hi1; move: Hi1 => /ltP Hi1.
 contradict Hx; apply /negP /negPn.
-rewrite -H nth_rcons; case_eq (i < size (rcons l y)); intros Hi2.
+rewrite -H nth_rcons; case_eq (i < size (rcons s y)); intros Hi2.
 clear x H; apply mem_nth; easy.
 contradict Hi1; apply /negP; apply negbT; easy.
 Qed.
 
 Lemma nth_rcons_r_rev_uniq :
-  forall {x0 x : T} {l : seq T} {i},
-    uniq (rcons l x) -> i <= size l -> nth x0 (rcons l x) i = x -> i = size l.
+  uniq (rcons l x) -> i <= size l -> nth x0 (rcons l x) i = x -> i = size l.
 Proof.
 move=>>; rewrite rcons_uniq.
 move=> /andP [Hx _]; apply nth_rcons_r_rev; easy.
 Qed.
 
+End Seq_compl2.
+
+
+Section Seq_compl3.
+
+Context {T : eqType}.
+
 Lemma injS_equiv_seq :
   forall {P : pred T} {sT : subType (T:=T) P} {f : T -> sT},
     injS P f <-> forall s, all P s -> { in s &, injective f }.
@@ -130,7 +134,7 @@ rewrite !in_cons eq_refl; apply orTb.
 rewrite !in_cons eq_refl; apply orbT.
 Qed.
 
-End Seq_compl2.
+End Seq_compl3.
 
 
 Section Ord_compl1.
@@ -601,7 +605,6 @@ Section Ord_compl2.
 
 Context {T : Type}.
 
-Variable leT : rel T.
 Variable x0 : T.
 
 Lemma size_ord_enum : forall {n}, size (ord_enum n) = n.
@@ -625,6 +628,23 @@ intros l; move: (map_nth_iota0 x0 (leqnn (size l))).
 rewrite take_size -val_ord_enum -map_comp; easy.
 Qed.
 
+Lemma map_nth_invF :
+  forall {n l1 l2}, size l1 = n.+1 -> size l2 = n.+1 ->
+    forall {p : 'I_[n.+1]} (Hp : injective p),
+      let q := f_inv (injF_bij Hp) in
+      l2 = map ((nth x0 l1) \o p) (ord_enum n.+1) ->
+      l1 = map ((nth x0 l2) \o q) (ord_enum n.+1).
+Proof.
+intros n l1 l2 Hl1 Hl2 p Hp q H.
+apply (@eq_from_nth _ x0); [rewrite size_map size_ord_enum; easy |].
+intros i Hi; rewrite Hl1 in Hi; pose (ii := Ordinal Hi).
+assert (Hii : val ii < size (ord_enum n.+1)) by now rewrite size_ord_enum.
+assert (Hq : forall j : 'I_n.+1, q j < size (ord_enum n.+1))
+    by now rewrite size_ord_enum.
+rewrite H; unfold comp; replace i with (val ii) by easy.
+rewrite !(nth_map ord0)// !nth_ord_enum f_inv_correct_r; easy.
+Qed.
+
 Definition in_ordS {n} (j : nat) : 'I_n.+1 :=
   match (lt_dec j n.+1) with
   | left Hj => Ordinal (lt_ltn Hj)
@@ -669,6 +689,16 @@ rewrite (nth_iota _ _ Hj) -add0n_sym nth_ord_enum_alt.
 apply in_ordS_correct_l_alt.
 Qed.
 
+End Ord_compl2.
+
+
+Section Ord_compl3a.
+
+Context {T : Type}.
+
+Variable leT : rel T.
+Variable x0 : T.
+
 Lemma perm_ord_enum_sort :
   forall l,
     { il | perm_eq il (ord_enum (size l)) /\ uniq il &
@@ -695,10 +725,10 @@ apply (@proj2 (0 <= nth 0 jl j)); apply /andP.
 rewrite -mem_iota -(perm_mem Hjl2 (nth 0 jl j)); apply mem_nth; easy.
 Qed.
 
-End Ord_compl2.
+End Ord_compl3a.
 
 
-Section Ord_compl3.
+Section Ord_compl3b.
 
 Context {T : eqType}.
 Context {leT : rel T}.
@@ -731,112 +761,47 @@ destruct (perm_ord_enum_sort leT x0 l1) as [il1 [Hil1a Hil1b] Hil1c].
 rewrite Hlb in il1, Hil1a, Hil1b, Hil1c; fold In in Hil1a; rewrite Hsa in Hil1c.
 assert (Hil1d : size il1 = n.+1) by now rewrite (perm_size Hil1a) size_ord_enum.
 pose (p1 := fun i : 'I_n.+1 => nth ord0 il1 i).
-assert (Hil1e : il1 = map p1 In).
-  unfold p1, In; move: (map_nth_ord_enum ord0 il1) => H.
-  rewrite -{1}H Hil1d; easy.
-rewrite Hil1e in Hil1c.
 assert (Hp1 : injective p1)
   by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil1d.
 pose (q1 := f_inv (injF_bij Hp1) : 'I_[n.+1]).
-assert (Hs1 : l1 = map ((nth x0 s) \o q1) In).
-  apply (@eq_from_nth _ x0).
-  rewrite size_map size_ord_enum; easy.
-  intros i Hi; rewrite Hlb in Hi; pose (ii := Ordinal Hi).
-  assert (Hii : val ii < size In) by now rewrite size_ord_enum.
-  assert (Hq1ii : q1 ii < size In) by now rewrite size_ord_enum.
-  replace i with (val ii) by easy.
-  rewrite (nth_map ord0)//.
-  rewrite nth_ord_enum comp_correct Hil1c (nth_map ord0);
-      [f_equal | rewrite size_map; easy].
-  rewrite (nth_map ord0)// nth_ord_enum f_inv_correct_r; easy.
+assert (Hil1e : il1 = map p1 In).
+  unfold p1, In; move: (map_nth_ord_enum ord0 il1) => H.
+  rewrite -{1}H Hil1d; easy.
+rewrite Hil1e -map_comp in Hil1c.
+assert (Hs1 : l1 = map ((nth x0 s) \o q1) In) by now apply map_nth_invF.
 (* il2 and p2/q2. *)
 destruct (perm_ord_enum_sort leT x0 l2) as [il2 [Hil2a Hil2b] Hil2c].
 rewrite Hn in il2, Hil2a, Hil2b, Hil2c; fold In in Hil2a; fold s in Hil2c.
 assert (Hil2d : size il2 = n.+1) by now rewrite (perm_size Hil2a) size_ord_enum.
 pose (p2 := fun i : 'I_n.+1 => nth ord0 il2 i).
-assert (Hil2e : il2 = map p2 In).
-  unfold p2, In; move: (map_nth_ord_enum ord0 il2) => H.
-  rewrite -{1}H Hil2d; easy.
-rewrite Hil2e in Hil2c.
 assert (Hp2 : injective p2)
   by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil2d.
 pose (q2 := f_inv (injF_bij Hp2) : 'I_[n.+1]).
-assert (Hs2 : l2 = map ((nth x0 s) \o q2) In).
-  apply (@eq_from_nth _ x0).
-  rewrite size_map size_ord_enum; easy.
-  intros i Hi; rewrite Hn in Hi; pose (ii := Ordinal Hi).
-  assert (Hii : val ii < size In) by now rewrite size_ord_enum.
-  assert (Hq2ii : q2 ii < size In) by now rewrite size_ord_enum.
-  replace i with (val ii) by easy.
-  rewrite (nth_map ord0)//.
-  rewrite nth_ord_enum comp_correct Hil2c (nth_map ord0);
-      [f_equal | rewrite size_map; easy].
-  rewrite (nth_map ord0)// nth_ord_enum f_inv_correct_r; easy.
+assert (Hil2e : il2 = map p2 In).
+  unfold p2, In; move: (map_nth_ord_enum ord0 il2) => H.
+  rewrite -{1}H Hil2d; easy.
+rewrite Hil2e -map_comp in Hil2c.
+assert (Hs2 : l2 = map ((nth x0 s) \o q2) In) by now apply map_nth_invF.
 (* *)
-exists (q2 \o p1); [apply inj_comp; [apply f_inv_inj | easy] |].
-rewrite map_comp.
-
-
-(*
-
-HERE!
-*)
-
-(*
-perm_eq mkseq map nth uniq
-drop take
-sort
-comp injective
-eq_from_nth
-
-perm_mem : perm_eq s1 s2 -> s1 =i s2
-perm_map : perm_eq s t -> perm_eq (map f s) (map f t)
-perm_map_inj : injective f -> perm_eq (map f s) (map f t) -> perm_eq s t
-perm_sortP : total leT -> transitive leT -> antisymmetric leT ->
-  reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2)
-nth_map : n < size s -> nth x2 (map f s) n = f (nth x1 s n)
-map_nth_iota0 : i <= size s -> map (nth x0 s) (iota 0 i) = take i s
-                --> map (nth x0 s) (iota 0 (size s)) = s
-nth_uniq : i < size s -> j < size s -> uniq s -> (nth x0 s i == nth x0 s j) = (i == j)
-sort_map : sort leT (map f s) = map f (sort (relpre f leT) s)
-*)
-Admitted.
+exists (p2 \o q1); [apply inj_comp; [easy | apply f_inv_inj] |].
+rewrite Hs1 Hs2; unfold comp.
+apply (@eq_from_nth _ x0); [rewrite !size_map; easy |].
+intros i Hi; rewrite size_map size_ord_enum in Hi; pose (ii := Ordinal Hi).
+assert (Hii : val ii < size In) by now rewrite size_ord_enum.
+replace i with (val ii) by easy.
+rewrite !(nth_map ord0)//; [| rewrite size_ord_enum; easy].
+rewrite !nth_ord_enum; unfold q2; rewrite f_inv_correct_l; easy.
+Qed.
 
 Lemma sort_perm_EX :
   forall l, { p : 'I_[size l] | injective p &
     sort leT l = map (fun i => nth x0 l (p i)) (ord_enum (size l)) }.
 Proof.
-(* Try to use perm_ord_enum_sort...
-intros l.
-destruct (perm_ord_enum_sort leT x0 l) as [il [Hil1 Hil2] Hil3].
-assert (Hil4 : size il = size l) by rewrite (perm_size Hil1) size_ord_enum//.
-*)
-
-(*
-pose (jl := map (cast_ord Hl) il).
-assert (Hjl1 : perm_eq jl (ord_enum n.+1)).
-  admit.
-assert (Hjl2 : uniq jl) by (rewrite map_inj_uniq; [easy | apply cast_ord_inj]).
-assert (Hjl4 : size jl = n.+1) by now rewrite size_map.
-exists (fun i : 'I_(size l) => nth ord0 il i); split.
-(* *)
-intros k1 k2 Hk.
-assert (Hk1 : k1 < size jl) by now destruct k1; rewrite Hjl4.
-assert (Hk2 : k2 < size jl) by now destruct k2; rewrite Hjl4.
-move: (nth_uniq ord0 Hk1 Hk2 Hjl2); rewrite Hk eq_refl.
-admit.
-(* *)
-unfold jl; rewrite Hil3 -2!map_comp.
-*)
-
-
-
-(* Proof using admitted perm_EX.*)
 intros l; destruct (perm_EX (permEl (perm_sort leT l))) as [p Hp1 Hp2].
 exists p; easy.
 Qed.
 
-End Ord_compl3.
+End Ord_compl3b.
 
 
 (** Specific ordinal transformations.