diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 01bb4516034d0307d97f16a4391422a5905c04e9..b39d793bd31ae85368300f6b83a3fd56fc619560 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -862,7 +862,7 @@ assert (Hil2e : il2 = map p2 In).
 rewrite Hil2e -map_comp in Hil2c.
 assert (Hs2 : l2 = map ((nth x0 s) \o q2) In) by now apply map_nth_invF.
 (* *)
-exists (p2 \o q1); [apply inj_comp; [easy | apply f_inv_inj] |].
+exists (p2 \o q1); [apply inj_comp_compat; [apply f_inv_inj | easy] |].
 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).
@@ -1666,7 +1666,7 @@ apply ord_not_max_lt in Hi0; destruct i0; simpl in *; auto with zarith.
 Qed.
 
 Lemma skip_ord_inj : forall {n} (i0 : 'I_n.+1), injective (skip_ord i0).
-Proof. intros; apply (inj_comp lift_inj), cast_ord_inj. Qed.
+Proof. intros; apply: inj_comp_compat lift_inj; apply cast_ord_inj. Qed.
 
 Lemma insert_ord_compat_P :
   forall {n} {i0 i : 'I_n.+1} (H H' : i <> i0), insert_ord H = insert_ord H'.
@@ -1839,7 +1839,7 @@ Qed.
 Lemma skip_f_ord_comp_alt :
   forall {n} {p q : 'I_[n.+1]}
       (Hp : injective p) (Hq : injective q) i0 j,
-    skip_f_ord (inj_comp Hp Hq) i0 j =
+    skip_f_ord (inj_comp_compat Hq Hp) i0 j =
       skip_f_ord Hp (q i0) (skip_f_ord Hq i0 j).
 Proof. intros; apply skip_f_ord_comp. Qed.
 
@@ -2021,7 +2021,7 @@ Qed.
 
 Lemma skip2_ord_inj :
   forall {n} {i0 i1 : 'I_n.+2} (H : i1 <> i0), injective (skip2_ord H).
-Proof. intros; apply (inj_comp (skip_ord_inj i0)), skip_ord_inj. Qed.
+Proof. intros; apply: (inj_comp_compat (skip_ord_inj _)) (skip_ord_inj _). Qed.
 
 Lemma insert_ord2_eq_lt :
   forall {n} {i0 i1 i : 'I_n.+2}
@@ -2771,7 +2771,7 @@ intros i [j _]; split; [move: (lift_S_not_first j) | apply filterP_ord_correct].
 rewrite -(filterP_ord_ind_l_in_0 _
     (cast_ord (sym_eq (lenPF_ind_l_in HP)) ord0)); [| apply cast_ordKV].
 rewrite -!(comp_correct _ filterP_ord); apply inj_contra.
-apply inj_comp; [apply filterP_ord_inj | apply cast_ord_inj].
+apply inj_comp_compat; [apply cast_ord_inj | apply filterP_ord_inj].
 (* *)
 intros i [Hi1 Hi2].
 assert (Hj : cast_ord (lenPF_ind_l_in HP) (unfilterP_ord HP i) <> ord0).
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 50aa3bdaa0beb36a5613c09400110757b1e68f2a..b09944db62d396f604834cfc24294ff87fbe7be8 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -300,7 +300,7 @@ End Range_Facts.
 
 Section Inj_Facts.
 
-Context {T1 T2 : Type}.
+Context {T1 T2 T3 : Type}.
 Context {f : T1 -> T2}.
 
 Lemma fun_from_empty_is_inj : ~ inhabited T1 -> injective f.
@@ -319,6 +319,10 @@ Proof. split; [apply inj_contra | apply inj_contra_rev]. Qed.
 Lemma inj_equiv : injective f -> forall x1 y1, f x1 = f y1 <-> x1 = y1.
 Proof. intros Hf x1 y1; split; [apply Hf | apply f_equal]. Qed.
 
+Lemma inj_ext :
+  forall {g : T1 -> T2}, same_fun f g -> injective f -> injective g.
+Proof. move=>> H Hf; apply (eq_inj Hf H). Qed.
+
 Lemma inj_has_left_inv : inhabited T1 -> injective f <-> exists g, cancel f g.
 Proof.
 intros [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
@@ -330,6 +334,13 @@ intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1];
     [apply Hf | contradict H1; rewrite not_all_not_ex_equiv; exists x1]; easy.
 Qed.
 
+Lemma inj_comp_compat :
+  forall {g : T2 -> T3}, injective f -> injective g -> injective (g \o f).
+Proof. intros; apply inj_comp; easy. Qed.
+
+Lemma inj_comp_reg : forall (g : T2 -> T3), injective (g \o f) -> injective f.
+Proof. intros g H; apply (inj_compr H). Qed.
+
 End Inj_Facts.
 
 
@@ -384,6 +395,10 @@ Section Can_Facts2.
 Context {T1 T2 : Type}.
 Context {f : T1 -> T2}.
 
+Lemma inj_can_uniq_l :
+  forall {g h : T2 -> T1}, injective f -> cancel g f -> cancel h f -> g = h.
+Proof. move=>> Hf Hg Hh; apply fun_ext, (inj_can_eq Hg Hf Hh). Qed.
+
 Lemma surj_can_uniq_r :
   forall {g h : T2 -> T1}, surjective f -> cancel f g -> cancel f h -> g = h.
 Proof.
@@ -468,7 +483,7 @@ Qed.
 
 Lemma f_inv_uniq_r : forall (g : T2 -> T1), cancel g f -> g = f_inv Hf.
 Proof.
-move=>> Hg; apply fun_ext, (inj_can_eq Hg);
+move=>> Hg; apply: (inj_can_uniq_l _ Hg);
     [apply bij_inj; easy | apply f_inv_correct_r].
 Qed.