diff --git a/FEM/Algebra/AffineSpace.v b/FEM/Algebra/AffineSpace.v
index bde5b09a4f4d827a8beff8845864024da3794a4b..3f2d965f816fc618fd8614d8c26277b94953cc91 100644
--- a/FEM/Algebra/AffineSpace.v
+++ b/FEM/Algebra/AffineSpace.v
@@ -1605,7 +1605,7 @@ apply unfun0F_ub; easy.
 apply barycenter_correct_equiv; try easy; unfold is_comb_aff.
 rewrite -comb_lin_filter_n0F_l filter_n0F_unfun0F.
 pose (Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf'))); fold Hg1.
-pose (g := f_inv Hg1); pose (Hg := bij_inj (f_inv_bij Hg1)); fold g Hg.
+pose (g := f_inv Hg1); pose (Hg := f_inv_inj Hg1); fold g Hg.
 rewrite 2!comb_lin_castF_l.
 rewrite -(comb_lin_permutF Hg) -comb_lin_filter_n0F_l in HG1.
 rewrite -HG1; f_equal; rewrite -castF_sym_equiv.
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index b5942d0ac60cc0a5dd405b773717952c19e63c7d..a1cdca96ab224502a3c5b39a65dd5f49cca8af19 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -284,11 +284,15 @@ Definition tripleF (x0 x1 x2 : E) : 'E^3 :=
     | inright _ => x2
     end.
 
-Definition inF {n} x (A : 'E^n) := exists i, x = A i.
+Definition inF {n} x (A : 'E^n) : Prop := exists i, x = A i.
 
-Definition inclF {n} (A : 'E^n) (PE : E -> Prop) := forall i, PE (A i).
+Definition inclF {n} (A : 'E^n) (PE : E -> Prop) : Prop := forall i, PE (A i).
 
-Definition invalF {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2) := inclF A1 (inF^~ A2).
+Definition invalF {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2) : Prop :=
+  inclF A1 (inF^~ A2).
+
+Definition eqF {n} (A : 'E^n) x i : Prop := A i = x.
+Definition neqF {n} (A : 'E^n) x i : Prop := A i <> x.
 
 Definition equivF {n} (P Q : 'Prop^n) := forall i, P i <-> Q i.
 
@@ -431,17 +435,17 @@ Section FF_ops_Def2.
 Context {E : Type}.
 
 Definition filter_eqF_gen {F : Type} {n} (A : 'E^n) (x0 : E) (B : 'F^n) :=
-  filterPF (fun i => A i = x0) B.
+  filterPF (eqF A x0) B.
 
 Definition filter_eqF {n} (A : 'E^n) (x0 : E) := filter_eqF_gen A x0 A.
 
 Definition filter_neqF_gen {F : Type} {n} (A : 'E^n) (x0 : E) (B : 'F^n) :=
-  filterPF (fun i => A i <> x0) B.
+  filterPF (neqF A x0) B.
 
 Definition filter_neqF {n} (A : 'E^n) (x0 : E) := filter_neqF_gen A x0 A.
 
 Definition split_eqF_gen {F : Type} {n} (A : 'E^n) (x0 : E) (B : 'F^n) :=
-  splitPF (fun i => A i = x0) B.
+  splitPF (eqF A x0) B.
 
 Definition split_eqF {n} (A : 'E^n) (x0 : E) := split_eqF_gen A x0 A.
 
@@ -1464,7 +1468,7 @@ assert (Hp1b : cancel p1 p).
   rewrite H transp_ord_correct_l0// transp_ord_correct_l1//.
   apply (f_inv_neq_equiv Hp'1) in Ha; rewrite (transp_ord_correct_r Ha _).
   apply f_inv_neq_equiv in Ha; rewrite f_inv_correct_r transp_ord_correct_r//.
-  contradict Hb; apply (bij_inj (f_inv_bij Hp'1)); easy.
+  contradict Hb; apply (f_inv_inj Hp'1); easy.
 apply (Bijective Hp1a Hp1b).
 (* *)
 unfold p, widenF in *; move: Hp'1 => /bij_equiv [Hp'1 _].
@@ -1522,10 +1526,17 @@ Context {E : Type}.
 
 (** Properties of operators funF/unfunF/maskPF. *)
 
-Lemma funF_neq :
+Lemma funF_equiv :
+  forall {n1 n2} (f : 'I_{n1,n2}) (A1 : 'E^n1) (A2 : 'E^n2),
+    funF f A2 = A1 <-> (forall i1 i2, i2 = f i1 -> A2 i2 = A1 i1).
+Proof.
+intros; split; intros HA. intros; subst; easy.
+apply extF; intros i1; apply (HA i1 (f i1)); easy.
+Qed.
+
+Lemma funF_neqF :
   forall {n1 n2} {f : 'I_{n1,n2}} {A2 : 'E^n2} {x0},
-    injective f ->
-    funF f (fun i2 => A2 i2 <> x0) = fun i1 => funF f A2 i1 <> x0.
+    funF f (neqF A2 x0) = neqF (funF f A2) x0.
 Proof. easy. Qed.
 
 Lemma unfunF_nil :
@@ -1581,12 +1592,11 @@ assert (~ (cast_ord (eq_sym (inj_ord_plus_minus_r Hf))
 rewrite concatF_correct_r; easy.
 Qed.
 
-Lemma unfunF_neq :
+Lemma unfunF_neqF :
   forall {n1 n2} {f : 'I_{n1,n2}} {A1 : 'E^n1} {x0},
-    injective f ->
-    unfunF f (fun i1 => A1 i1 <> x0) False = fun i2 => unfunF f A1 x0 i2 <> x0.
+    injective f -> unfunF f (neqF A1 x0) False = neqF (unfunF f A1 x0) x0.
 Proof.
-intros n1 n2 f A1 x0 Hf; apply extF; intros i2;
+intros n1 n2 f A1 x0 Hf; apply extF; intros i2; unfold neqF;
     destruct (unfunF_correct A1 x0 i2 Hf) as [[i1 [-> ->]] | [Hi2 ->]].
 rewrite (unfunF_correct_l _ i1); easy.
 rewrite unfunF_correct_r; [apply propositional_extensionality |]; easy.
@@ -4333,7 +4343,7 @@ Context {E : Type}.
 Lemma len_neqF_concatF_l :
   forall {n1 n2} (A1 : 'E^n1) {A2 : 'E^n2} {x0},
     A2 = constF n2 x0 ->
-    lenPF (fun i => concatF A1 A2 i <> x0) = lenPF (fun i1 => A1 i1 <> x0).
+    lenPF (neqF (concatF A1 A2) x0) = lenPF (neqF A1 x0).
 Proof.
 Aglopted.
 
@@ -4346,7 +4356,7 @@ Aglopted.
 
 Lemma len_neqF_concatF_r :
   forall {n1 n2} {A1 : 'E^n1} {x0}, A1 = constF n1 x0 -> forall (A2 : 'E^n2),
-    lenPF (fun i => concatF A1 A2 i <> x0) = lenPF (fun i2 => A2 i2 <> x0).
+    lenPF (neqF (concatF A1 A2) x0) = lenPF (neqF A2 x0).
 Proof.
 Aglopted.
 
@@ -4409,23 +4419,61 @@ Definition extendPF {n1 n2} (f : 'I_{n1,n2})
     (P1 : 'Prop^n1) (P2 : 'Prop^n2) : Prop :=
   forall i2, (exists i1, i2 = f i1 /\ P2 i2 = P1 i1) \/ (~ Rg f i2 /\ ~ P2 i2).
 
+(* Note that incl P2 (Rg f) <-> forall i2, ~ Rg f i2 -> ~ P2 i2. *)
 Lemma extendPF_funF :
   forall {n1 n2} {f : 'I_{n1,n2}} {P2 : 'Prop^n2},
-    injective f -> (forall i2, ~ Rg f i2 -> ~ P2 i2) ->
-    extendPF f (funF f P2) P2.
+    injective f -> incl P2 (Rg f) -> extendPF f (funF f P2) P2.
 Proof.
-intros n1 n2 f P2 Hf HP2 i2; destruct (im_dec f i2) as [[i1 ->] | Hi2].
+move=> n1 n2 f P2 Hf /compl_monot HP2 i2;
+    destruct (im_dec f i2) as [[i1 ->] | Hi2].
 left; exists i1; easy.
-right; split; [| apply HP2]; rewrite Rg_compl; easy.
+right; split; [| apply HP2; unfold compl]; rewrite Rg_compl; easy.
+Qed.
+
+Lemma extendPF_funF_rev :
+  forall {n1 n2} {f : 'I_{n1,n2}} {P1 : 'Prop^n1} {P2 : 'Prop^n2},
+    injective f -> extendPF f P1 P2 -> P1 = funF f P2 /\ incl P2 (Rg f).
+Proof.
+intros n1 n2 f P1 P2 Hf HP; split.
+(* *)
+apply extF; intros i1; destruct (HP (f i1)) as [[i1' [Hi1'a Hi1'b]] | [Hi1 _]].
+apply Hf in Hi1'a; subst; easy.
+contradict Hi1; easy.
+(* *)
+apply incl_compl_equiv; unfold compl.
+intros i2 Hi2. destruct (HP i2) as [[i1 [Hi1 _]] | Hi2'];
+    [contradict Hi2; subst |]; easy.
+Qed.
+
+Lemma extendPF_funF_equiv :
+  forall {n1 n2} {f : 'I_{n1,n2}} {P1 : 'Prop^n1} {P2 : 'Prop^n2},
+    injective f -> extendPF f P1 P2 <-> P1 = funF f P2 /\ incl P2 (Rg f).
+Proof.
+intros; split; [apply extendPF_funF_rev |
+    intros [HP1 HP2]; subst; apply extendPF_funF]; easy.
 Qed.
 
-Lemma extendPF_funF_neq :
+Lemma extendPF_funF_neqF :
+  forall {n1 n2} {f : 'I_{n1,n2}} {A2 : 'E^n2} {x0},
+    injective f -> incl (neqF A2 x0) (Rg f) ->
+    extendPF f (neqF (funF f A2) x0) (neqF A2 x0).
+Proof. move=>> Hf HA2; rewrite -funF_neqF; apply (extendPF_funF Hf HA2). Qed.
+
+Lemma extendPF_funF_neqF_rev :
   forall {n1 n2} {f : 'I_{n1,n2}} {A2 : 'E^n2} {x0},
-    injective f -> (forall i2, ~ Rg f i2 -> A2 i2 = x0) ->
-    extendPF f (fun i1 => funF f A2 i1 <> x0) (fun i2 => A2 i2 <> x0).
+    injective f ->
+    extendPF f (neqF (funF f A2) x0) (neqF A2 x0) -> incl (neqF A2 x0) (Rg f).
+Proof. move=>> Hf /(extendPF_funF_rev Hf) HA2; easy. Qed.
+
+Lemma extendPF_funF_neqF_equiv :
+  forall {n1 n2} {f : 'I_{n1,n2}} {A2 : 'E^n2} {x0},
+    injective f ->
+    extendPF f (neqF (funF f A2) x0) (neqF A2 x0) <->
+    incl (neqF A2 x0) (Rg f).
 Proof.
-move=>> Hf HA2; rewrite -(funF_neq Hf); apply (extendPF_funF Hf).
-intros; apply PNNP; auto.
+move=>> Hf; rewrite (extendPF_funF_equiv Hf).
+assert (H : forall P Q : Prop, P -> P /\ Q <-> Q) by tauto.
+apply H, sym_eq, funF_neqF.
 Qed.
 
 Lemma extendPF_unfunF :
@@ -4439,7 +4487,7 @@ right; split; [rewrite Rg_compl |]; easy.
 Qed.
 
 Lemma extendPF_unfunF_rev :
-  forall {n1 n2} {f : 'I_{n1,n2}} (P1 : 'Prop^n1) (P2 : 'Prop^n2),
+  forall {n1 n2} {f : 'I_{n1,n2}} {P1 : 'Prop^n1} {P2 : 'Prop^n2},
     injective f -> extendPF f P1 P2 -> P2 = unfunF f P1 False.
 Proof.
 move=>> Hf HP; apply extF; intros i2;
@@ -4448,19 +4496,21 @@ rewrite (unfunF_correct_l _ i1); easy.
 rewrite unfunF_correct_r; [apply boolp.notTE | rewrite -Rg_compl]; easy.
 Qed.
 
-Lemma extendPF_equiv :
-  forall {n1 n2} {f : 'I_{n1,n2}} (P1 : 'Prop^n1) (P2 : 'Prop^n2),
+Lemma extendPF_unfunF_equiv :
+  forall {n1 n2} {f : 'I_{n1,n2}} {P1 : 'Prop^n1} {P2 : 'Prop^n2},
     injective f -> extendPF f P1 P2 <-> P2 = unfunF f P1 False.
 Proof.
 intros; split; [apply extendPF_unfunF_rev |
     intros; subst; apply extendPF_unfunF]; easy.
 Qed.
 
-Lemma extendPF_unfunF_neq :
+Lemma extendPF_unfunF_neqF :
   forall {n1 n2} {f : 'I_{n1,n2}} (A1 : 'E^n1) x0,
     injective f ->
-    extendPF f (fun i1 => A1 i1 <> x0) (fun i2 => unfunF f A1 x0 i2 <> x0).
-Proof. move=>> Hf; rewrite -(unfunF_neq Hf); apply (extendPF_unfunF _ Hf). Qed.
+    extendPF f (neqF A1 x0) (neqF (unfunF f A1 x0) x0).
+Proof.
+move=>> Hf; apply (extendPF_unfunF_equiv Hf), sym_eq, (unfunF_neqF Hf).
+Qed.
 
 Lemma lenPF_extendPF :
   forall {n1 n2} {f : 'I_{n1,n2}} {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop},
@@ -4502,8 +4552,18 @@ Lemma filterPF_funF :
       {P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2) (A2 : 'F^n2),
     filterPF P1 (funF f A2) =
       castF (sym_eq (lenPF_extendPF Hf HP)) (filterPF P2 A2).
+(* Should try something as (with some i0):
+    let p := proj1_sig (injF_restr_bij_EX Hf) in
+    let Hp := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+    let p1 := f_inv Hp in
+    let Hp1 := f_inv_inj Hp in
+    forall (HP0 : P1 i0), (* to be fixed! *)
+      filterPF P1 (funF f A2) =
+        funF (filterP_f_ord p p1 HP0) (filterPF P2 A2).
+*)
 Proof.
-intros F n1 n2 f Hf P1 P2 HP A2; apply extF; intros j1; rewrite castF_eq_sym.
+intros F n1 n2 f Hf P1 P2 HP A2.
+apply extF; intros j1. rewrite castF_eq_sym.
 unfold filterPF, funF; f_equal.
 
 
@@ -4515,25 +4575,25 @@ Admitted.
 
 Lemma len_neqF_funF :
   forall {n1 n2} {f : 'I_{n1,n2}} {A2 : 'E^n2} {x0},
-    injective f -> (forall i2, ~ Rg f i2 -> A2 i2 = x0) ->
-    lenPF (fun i1 => funF f A2 i1 <> x0) = lenPF (fun i2 => A2 i2 <> x0).
+    injective f -> incl (neqF A2 x0) (Rg f) ->
+    lenPF (neqF (funF f A2) x0) = lenPF (neqF A2 x0).
 Proof.
-move=>> Hf HA2; apply (lenPF_extendPF Hf), (extendPF_funF_neq Hf HA2).
+move=>> Hf HA2; apply (lenPF_extendPF Hf), (extendPF_funF_neqF_equiv Hf); easy.
 Qed.
 
 Lemma filter_neqF_gen_funF :
   forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
-      {A2 : 'E^n2} {x0} {B2 : 'F^n2} (HA2 : forall i2, ~ Rg f i2 -> A2 i2 = x0),
+      {A2 : 'E^n2} {x0} {B2 : 'F^n2} (HA2 : incl (neqF A2 x0) (Rg f)),
     filter_neqF_gen (funF f A2) x0 (funF f B2) =
       castF (sym_eq (len_neqF_funF Hf HA2)) (filter_neqF_gen A2 x0 B2).
 Proof.
 intros F n1 n2 f Hf A2 x0 B2 HA2; unfold filter_neqF_gen.
-rewrite (filterPF_funF Hf (extendPF_funF_neq Hf HA2)); apply castF_eq_r; easy.
+rewrite (filterPF_funF Hf (extendPF_funF_neqF Hf HA2)); apply castF_eq_r; easy.
 Qed.
 
 Lemma filter_neqF_gen_funF_r :
   forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
-      {A2 : 'E^n2} {x0} {B1 : 'F^n1} y0 (HA2 : forall i2, ~ Rg f i2 -> A2 i2 = x0),
+      {A2 : 'E^n2} {x0} {B1 : 'F^n1} y0 (HA2 : incl (neqF A2 x0) (Rg f)),
     filter_neqF_gen (funF f A2) x0 B1 =
       castF (sym_eq (len_neqF_funF Hf HA2)) (filter_neqF_gen A2 x0 (unfunF f B1 y0)).
 Proof.
@@ -4543,15 +4603,17 @@ Qed.
 
 Lemma filter_neqF_funF :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f) (A2 : 'E^n2) x0
-      (HA2 : forall i2, ~ Rg f i2 -> A2 i2 = x0),
+      (HA2 : incl (neqF A2 x0) (Rg f)),
     filter_neqF (funF f A2) x0 =
       castF (sym_eq (len_neqF_funF Hf HA2)) (filter_neqF A2 x0).
 Proof.
-intros n1 n2 f Hf A2 x0 HA2; unfold filter_neqF.
+move=> n1 n2 f Hf A2 x0 HA2; unfold filter_neqF.
 rewrite (filter_neqF_gen_funF_r Hf x0) (unfunF_funF _ Hf); repeat f_equal.
 apply extF; intros i2; destruct (im_dec f i2) as [[i1 ->] | Hi2].
 apply maskPF_correct_l; easy.
-rewrite (HA2 i2); [ apply maskPF_correct_r; rewrite -Rg_compl_equiv |];
+rewrite -incl_compl_equiv in HA2; specialize (HA2 i2);
+    unfold compl, neqF in HA2; rewrite NNPP_equiv in HA2.
+rewrite HA2; [ apply maskPF_correct_r; rewrite -Rg_compl_equiv |];
     rewrite Rg_compl; easy.
 Qed.
 
@@ -4563,16 +4625,16 @@ Lemma filterPF_unfunF :
     P1 i0 ->
     let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
     let g := f_inv Hg1 in
-    let Hg := bij_inj (f_inv_bij Hg1) in
+    let Hg := f_inv_inj Hg1 in
     filterPF P2 (unfunF f A1 x0) =
       castF (lenPF_extendPF Hf HP) (castF (lenPF_permutF Hg)
         (filterPF (permutF g P1) (permutF g A1))).
 Proof.
 intros F n1 n2 f P1 P2 Hf HP A1 x0 i0 HP1 Hg1 g Hg.
 pose (p := proj1_sig (injF_restr_bij_EX Hf)); pose (i1 := p i0).
-assert (HP0 : permutF g P1 i1).
+assert (HP1' : permutF g P1 i1).
   unfold permutF, i1, g; rewrite f_inv_correct_l; easy.
-rewrite (filterPF_permutF Hg HP0).
+rewrite (filterPF_permutF Hg HP1').
 apply sym_eq; rewrite castF_sym_equiv -(filterPF_funF Hf HP) funF_unfunF//.
 apply extF; intros j1; unfold castF, funF.
 f_equal; unfold filterP_f_ord; rewrite f_inv_invol.
@@ -4589,16 +4651,17 @@ Admitted.
 
 Lemma len_neqF_unfunF :
   forall {n1 n2} {f : 'I_{n1,n2}} {A1 : 'E^n1} {x0},
-    injective f ->
-    lenPF (fun i1 => A1 i1 <> x0) = lenPF (fun i2 => unfunF f A1 x0 i2 <> x0).
-Proof. move=>> Hf; apply (lenPF_extendPF Hf), (extendPF_unfunF_neq _ _ Hf). Qed.
+    injective f -> lenPF (neqF A1 x0) = lenPF (neqF (unfunF f A1 x0) x0).
+Proof.
+move=>> Hf; apply (lenPF_extendPF Hf), (extendPF_unfunF_neqF _ _ Hf).
+Qed.
 
 Lemma filter_neqF_gen_unfunF :
   forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
       (A1 : 'E^n1) x0 (B1 : 'F^n1) y0,
     let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
     let g := f_inv Hg1 in
-    let Hg := bij_inj (f_inv_bij Hg1) in
+    let Hg := f_inv_inj Hg1 in
     filter_neqF_gen (unfunF f A1 x0) x0 (unfunF f B1 y0) =
       castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hg)
         (filter_neqF_gen (permutF g A1) x0 (permutF g B1))).
@@ -4607,7 +4670,7 @@ intros F n1 n2 f Hf A1 x0 B1 y0 Hg1 g Hg.
 destruct (excluded_middle_informative (forall i1, A1 i1 = x0)) as [HA1 | HA1].
 apply eqAF_nil; left; apply lenPF0_alt; intuition.
 move: HA1 => /not_all_ex_not_equiv [i0 Hi0].
-move: (extendPF_unfunF_neq A1 x0 Hf) => H0.
+move: (extendPF_unfunF_neqF A1 x0 Hf) => H0.
 unfold filter_neqF_gen; rewrite (filterPF_unfunF Hf H0 _ _ i0);
     [rewrite !castF_comp; apply castF_eq_r |]; easy.
 Qed.
@@ -4617,7 +4680,7 @@ Lemma filter_neqF_gen_unfunF_l :
       {f : 'I_{n1,n2}} (Hf : injective f) (A1 : 'E^n1) x0 (B2 : 'F^n2),
     let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
     let g := f_inv Hg1 in
-    let Hg := bij_inj (f_inv_bij Hg1) in
+    let Hg := f_inv_inj Hg1 in
     filter_neqF_gen (unfunF f A1 x0) x0 B2 =
       castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hg)
         (filter_neqF_gen (permutF g A1) x0 (permutF g (funF f B2)))).
@@ -4632,7 +4695,7 @@ Lemma filter_neqF_unfunF :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f) (A1 : 'E^n1) x0,
     let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
     let g := f_inv Hg1 in
-    let Hg := bij_inj (f_inv_bij Hg1) in
+    let Hg := f_inv_inj Hg1 in
     filter_neqF (unfunF f A1 x0) x0 =
       castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hg)
         (filter_neqF (permutF g A1) x0)).
diff --git a/FEM/Algebra/Monoid_compl.v b/FEM/Algebra/Monoid_compl.v
index 0372f9cf758a4212c3743c85039f1c1799252a86..47cb7e88b2eb3e2ef47410b93ae297408e0f1b43 100644
--- a/FEM/Algebra/Monoid_compl.v
+++ b/FEM/Algebra/Monoid_compl.v
@@ -582,7 +582,7 @@ Lemma filter_n0F_gen_unfun0F :
       (u1 : 'G^n1) (v1 : 'H^n1),
     let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
     let g := f_inv Hg1 in
-    let Hg := bij_inj (f_inv_bij Hg1) in
+    let Hg := f_inv_inj Hg1 in
     filter_n0F_gen (unfun0F f u1) (unfun0F f v1) =
       castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hg)
         (filter_n0F_gen (permutF g u1) (permutF g v1))).
@@ -596,7 +596,7 @@ Lemma filter_n0F_gen_unfun0F_l :
       (u1 : 'G^n1) (u2 : 'H^n2),
     let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
     let g := f_inv Hg1 in
-    let Hg := bij_inj (f_inv_bij Hg1) in
+    let Hg := f_inv_inj Hg1 in
     filter_n0F_gen (unfun0F f u1) u2 =
       castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hg)
         (filter_n0F_gen (permutF g u1) (permutF g (funF f u2)))).
@@ -609,7 +609,7 @@ Lemma filter_n0F_unfun0F :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f) (u1 : 'G^n1),
     let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
     let g := f_inv Hg1 in
-    let Hg := bij_inj (f_inv_bij Hg1) in
+    let Hg := f_inv_inj Hg1 in
     filter_n0F (unfun0F f u1) =
       castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hg)
         (filter_n0F (permutF g u1))).
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index e14c00a52f27375cc66ad252fa85b5a61c59a4e0..1e6551607d9fafaaf1f08be81d0b36c2f8bcb380 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -1099,7 +1099,7 @@ Proof. intros; apply skip_f_ord_comp. Qed.
 
 Lemma skip_f_ord_f_inv :
   forall {n} {p : 'I_[n.+1]} (Hp : bijective p) i0,
-    skip_f_ord (bij_inj (f_inv_bij Hp)) i0 =
+    skip_f_ord (f_inv_inj Hp) i0 =
       f_inv (skip_f_ord_bij (bij_inj Hp) (f_inv Hp i0)).
 Proof.
 intros n p Hp i0; apply f_inv_uniq_l; intros j.
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index d667c333d044b8950bb26388d879a6b9ac2ab510..20f12c3141a6dc19e0344b1034a6173da8f4ad29 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -289,6 +289,12 @@ Qed.
 Lemma f_inv_bij : bijective f_inv.
 Proof. apply (bij_can_bij Hf), f_inv_correct_l. Qed.
 
+Lemma f_inv_inj : injective f_inv.
+Proof. apply bij_inj, f_inv_bij. Qed.
+
+Lemma f_inv_surj : surjective f_inv.
+Proof. apply bij_surj, f_inv_bij. Qed.
+
 Lemma f_inv_eq_equiv : forall x1 x2, f_inv x2 = x1 <-> x2 = f x1.
 Proof.
 intros x1 x2; split.