Function_sub:

Generalize funS_id.
Add and prove canS_id_{l,r}, bijS_id.

MonoidComp:
Propagate new APi (from Function_sub).

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).

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.