diff --git a/FEM/Algebra/MonoidComp.v b/FEM/Algebra/MonoidComp.v
index 548295d2c45eccd59330e25557edf5c0a457ca11..c3200bc4ad3ef8ad5b5771b0a6dc7e337085e394 100644
--- a/FEM/Algebra/MonoidComp.v
+++ b/FEM/Algebra/MonoidComp.v
@@ -216,7 +216,7 @@ Lemma comp_n_funS :
(forall i, funS PE PE (f i)) -> funS PE PE (comp_n f).
Proof.
intros n f Hf; induction n as [|n Hn];
- [rewrite comp_n_nil; [apply funS_id | easy] | rewrite comp_n_ind_l].
+ [rewrite comp_n_nil; [apply funS_id |]; easy | rewrite comp_n_ind_l].
apply (funS_comp_compat PE); [apply Hn; unfold liftF_S |]; easy.
Qed.
@@ -292,9 +292,9 @@ Lemma comp_n_part_funS :
funS PE PE (comp_n_part f j).
Proof.
intros n f j Hf; induction n as [|n Hn];
- [rewrite comp_n_part_nil; [apply funS_id | easy] |].
+ [rewrite comp_n_part_nil; [apply funS_id |]; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
- [rewrite (comp_n_part_0 _ _ Hj0); apply funS_id |].
+ [rewrite (comp_n_part_0 _ _ Hj0); apply funS_id; easy |].
rewrite comp_n_part_ind_l; apply (funS_comp_compat PE); [apply Hn |].
intros; apply (widenF_liftF_S_P_compat _ Hj0 Hf); easy.
apply (widenF_0_P_compat Hj0 Hf).
diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v
index 5afcaffd21933198918888c9d9fa6f9e6ccd54ab..f955325708a5bc176fe46d3ff65365391c5fcc77 100644
--- a/FEM/Compl/Function_sub.v
+++ b/FEM/Compl/Function_sub.v
@@ -292,10 +292,12 @@ Section FunS_Facts3.
Context {T : Type}.
-Variable P : T -> Prop.
+Context {P : T -> Prop}.
+
+Context {f : T -> T}.
-Lemma funS_id : funS P P id.
-Proof. apply funS_equiv; easy. Qed.
+Lemma funS_id : same_funS P f id -> funS P P f.
+Proof. intros Hf _ [y Hy]; rewrite Hf; easy. Qed.
End FunS_Facts3.
@@ -623,6 +625,23 @@ End SurjS_Facts7.
Section CanS_Facts1.
+Context {T : Type}.
+
+Context {P : T -> Prop}.
+
+Context {f : T -> T}.
+
+Lemma canS_id_l : same_funS P f (id : T -> T) -> canS P f id.
+Proof. easy. Qed.
+
+Lemma canS_id_r : same_funS P f (id : T -> T) -> canS P id f.
+Proof. easy. Qed.
+
+End CanS_Facts1.
+
+
+Section CanS_Facts2.
+
Context {T1 T2 : Type}.
Context {P1 : T1 -> Prop}.
@@ -638,10 +657,10 @@ Lemma canS_ext_r :
funS P1 P2 f -> same_funS P2 g g' -> canS P1 f g -> canS P1 f g'.
Proof. intros Hf Hg H x1 Hx1; rewrite -Hg//; [apply H | apply Hf]; easy. Qed.
-End CanS_Facts1.
+End CanS_Facts2.
-Section CanS_Facts2.
+Section CanS_Facts3.
Context {T1 T2 : Type}.
@@ -656,10 +675,10 @@ Lemma canS_ext :
canS P1 f g -> canS P1 f' g'.
Proof. move=> H1 H2 H3 /(canS_ext_r H1 H3) /(canS_ext_l H2); easy. Qed.
-End CanS_Facts2.
+End CanS_Facts3.
-Section CanS_Facts3.
+Section CanS_Facts4.
Context {T1 T2 : Type}.
@@ -704,10 +723,10 @@ intros Hf; exists (fun x2 => match imS_dec P1 f x2 with
exists x1; rewrite not_imp_not_r_and_equiv; easy.
Qed.
-End CanS_Facts3.
+End CanS_Facts4.
-Section CanS_Facts4.
+Section CanS_Facts5.
Context {T1 T2 : Type}.
@@ -724,10 +743,10 @@ intros H1 H2 H3 H4 x2 Hx2;
apply H3; [apply H1, Im | easy | rewrite H4//]; apply H2; easy.
Qed.
-End CanS_Facts4.
+End CanS_Facts5.
-Section CanS_Facts5.
+Section CanS_Facts6.
Context {T1 T2 T3 : Type}.
@@ -746,11 +765,28 @@ Proof.
move=> /funS_equiv H1 H2 H3 x1 Hx1; rewrite -> !comp_correct, H3, H2; auto.
Qed.
-End CanS_Facts5.
+End CanS_Facts6.
Section BijS_Facts1.
+Context {T : Type}.
+
+Context {P : T -> Prop}.
+
+Context {f : T -> T}.
+
+Lemma bijS_id : same_funS P f (id : T -> T) -> bijS P P f.
+Proof.
+intros; apply (BijS _ _ _ id); repeat split;
+ [apply funS_id.. | apply canS_id_l | apply canS_id_r]; easy.
+Qed.
+
+End BijS_Facts1.
+
+
+Section BijS_Facts2.
+
Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
@@ -769,10 +805,10 @@ apply (canS_ext_l Hg Hf3).
apply (canS_ext_r Hf2 Hg Hf4).
Qed.
-End BijS_Facts1.
+End BijS_Facts2.
-Section BijS_Facts2.
+Section BijS_Facts3.
Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
@@ -816,10 +852,10 @@ Lemma bijS_ex_uniq_equiv :
funS P1 P2 f /\ (forall x2, P2 x2 -> exists! x1, P1 x1 /\ f x1 = x2).
Proof. split; [apply bijS_ex_uniq | intros; apply bijS_ex_uniq_rev; easy]. Qed.
-End BijS_Facts2.
+End BijS_Facts3.
-Section BijS_Facts3.
+Section BijS_Facts4.
Context {T1 T2 : Type}.
@@ -846,10 +882,10 @@ Qed.
Lemma bijS_surjS : bijS P1 P2 f -> surjS P1 P2 f.
Proof. move=> [g [_ [/funS_equiv Hg [_ Hf]]]] x2 Hx2; exists (g x2); auto. Qed.
-End BijS_Facts3.
+End BijS_Facts4.
-Section BijS_Facts4.
+Section BijS_Facts5.
Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
@@ -874,10 +910,10 @@ split; [apply (bijS_injS P2) | apply bijS_surjS]; easy.
apply injS_surjS_bijS; easy.
Qed.
-End BijS_Facts4.
+End BijS_Facts5.
-Section BijS_Facts5.
+Section BijS_Facts6.
Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
@@ -895,10 +931,10 @@ Qed.
Lemma bij_S_equiv : bijective f <-> bijS fullset fullset f.
Proof. rewrite bij_equiv bijS_equiv// inj_S_equiv surj_S_equiv; easy. Qed.
-End BijS_Facts5.
+End BijS_Facts6.
-Section BijS_Facts6.
+Section BijS_Facts7.
Context {T1 T2 T3 : Type}.
Hypothesis HT1 : inhabited T1.
@@ -925,10 +961,10 @@ Proof.
intros [f1 Hf] [g1 Hg]; exists (f1 \o g1); apply bijS_spec_comp_compat; easy.
Qed.
-End BijS_Facts6.
+End BijS_Facts7.
-Section BijS_Facts7.
+Section BijS_Facts8.
Context {T1 T2 T3 : Type}.
Hypothesis HT1 : inhabited T1.
@@ -946,10 +982,10 @@ intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) => [_ [H3 _]].
apply injS_comp_reg with g; easy.
Qed.
-End BijS_Facts7.
+End BijS_Facts8.
-Section BijS_Facts8.
+Section BijS_Facts9.
Context {T1 T2 T3 : Type}.
Hypothesis HT1 : inhabited T1.
@@ -967,10 +1003,10 @@ intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) => [_ [_ H3]].
apply (surjS_comp_reg P1 f); easy.
Qed.
-End BijS_Facts8.
+End BijS_Facts9.
-Section BijS_Facts9.
+Section BijS_FactsA.
Context {T1 T2 : Type}.
@@ -989,10 +1025,10 @@ Lemma bijS_canS_uniq_r :
bijS P1 P2 f -> canS P1 f g -> canS P1 f h -> same_funS P2 g h.
Proof. move=> /bijS_surjS; apply surjS_canS_uniq_r. Qed.
-End BijS_Facts9.
+End BijS_FactsA.
-Section BijS_Facts10.
+Section BijS_FactsB.
Context {T1 T2 : Type}.
@@ -1021,7 +1057,7 @@ intros Hg Hf; apply bijS_ex; exists f; repeat split; [.. | easy].
apply (bijS_funS Hf).
Qed.
-End BijS_Facts10.
+End BijS_FactsB.
Section F_invS_Def.