diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 72cc88f2327b4d25d04222a944d79ee7a1e862e5..059dd8b70faddc510e9c24fad59ad3160e895c8c 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -617,6 +617,14 @@ Qed.
 Lemma nth_ord_enum : forall {n} i0 {i : 'I_n}, nth i0 (ord_enum n) i = i.
 Proof. intros n i0 [j Hj]; apply nth_ord_enum_alt. Qed.
 
+Lemma map_nth_ord_enum :
+  forall (l : seq T),
+    map (fun i : 'I_(size l) => nth x0 l i) (ord_enum (size l)) = l.
+Proof.
+intros l; move: (map_nth_iota0 x0 (leqnn (size l))).
+rewrite take_size -val_ord_enum -map_comp; easy.
+Qed.
+
 Definition in_ordS {n} (j : nat) : 'I_n.+1 :=
   match (lt_dec j n.+1) with
   | left Hj => Ordinal (lt_ltn Hj)
@@ -704,34 +712,72 @@ Variable x0 : T.
 Lemma perm_EX :
   forall {l1 l2}, perm_eq l1 l2 ->
     { p : 'I_[size l2] | injective p &
-      l1 = map (fun i => nth x0 l2 (p i)) (ord_enum (size l2)) }.
+      l1 = map ((nth x0 l2) \o p) (ord_enum (size l2)) }.
 Proof.
 intros l1 l2 Hla.
 assert (Hlb : size l1 = size l2) by now apply perm_size.
 pose (n := size l2); assert (Hn : size l2 = n) by easy.
 fold n in Hlb; fold n; destruct n as [|n].
-(* *)
+(* n=0 *)
 exists (fun_from_I_0 'I_0); [apply fun_from_I_0_inj |].
 rewrite (size0nil Hlb) (size0nil size_ord_enum); easy.
-(* *)
+(* n>0 *)
+pose (In1 := ord_enum n.+1); fold In1.
 move: (perm_sortP HT2 HT1 HT0 _ _ Hla) => Hlc.
+pose (s := sort leT l2); assert (Hs1 : sort leT l1 = s) by easy.
+assert (Hs2 : size s = n.+1) by now rewrite size_sort.
+(* il1 and p1. *)
 destruct (perm_ord_enum_sort leT x0 l1) as [il1 [Hil1a Hil1b] Hil1c].
-rewrite Hlb in il1, Hil1a, Hil1b, Hil1c.
-pose (p1 := fun i : 'I_n => nth ord0 il1 i).
+rewrite Hlb in il1, Hil1a, Hil1b, Hil1c; fold In1 in Hil1a; rewrite Hs1 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 (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 (Hs3 : l1 = map ((nth x0 s) \o q1) In1).
+  rewrite -(map_nth_ord_enum x0 (map _ _)).
+  
+
+
+(*
 destruct (perm_ord_enum_sort leT x0 l2) as [il2 [Hil2a Hil2b] Hil2c].
 rewrite Hn in il2, Hil2a, Hil2b, Hil2c.
-pose (p2 := fun i : 'I_n => nth ord0 il2 i).
+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 (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]).
+(* *)
+exists (q2 \o p1); [apply inj_comp; [apply f_inv_inj | easy] |].
+rewrite map_comp.
 
 
+replace (map (fun i : 'I_n.+1 => nth x0 l2 i) (map (q2 \o p1) (ord_enum n.+1)))
+    with (map (fun i : 'I_n.+1 => nth x0 l2 i) (map q2 (map p1 (ord_enum n.+1)))).
+rewrite (map_comp q2 p1).
+
+(_ -> _ = _) in seq
+
+HERE!
+*)
 
 (*
-perm_eq
+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.
 
@@ -739,10 +785,12 @@ 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...*)
+(* 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)).
@@ -762,11 +810,10 @@ unfold jl; rewrite Hil3 -2!map_comp.
 
 
 
-(* Proof using admitted perm_EX.
+(* Proof using admitted perm_EX.*)
 intros l; destruct (perm_EX (permEl (perm_sort leT l))) as [p Hp1 Hp2].
 exists p; easy.
-*)
-Admitted.
+Qed.
 
 End Ord_compl3.