diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 790c414deadd8ec25dcfd42b31ba59f5ae2e3045..cb6faa36693a3117f382bd2d5e1a251183f6725a 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -796,10 +796,7 @@ 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.
-intros l; destruct (perm_EX (permEl (perm_sort leT l))) as [p Hp1 Hp2].
-exists p; easy.
-Qed.
+Proof. intros l; apply (perm_EX (permEl (perm_sort leT l))). Qed.
 
 End Ord_compl3b.