logic_compl:

Add and prove imp_not_{l,r}_{and,or}_equiv,
              not_imp_not_{l,r}_{and,or}_equiv.

Function_compl:
Add and prove surj_can_uniq_r, inj_contra_{rev,equiv}.

Function_sub:
Add and prove imS_dec,
              injS_id, injS_contra{,_rev,_equiv}, injS_equiv,
              injS_canS_uniq_l, comp_injS_r, surjS_canS_uniq_r,
              injS_has_left_inv.

FEM/Compl/Function_compl.v

@@ -251,6 +251,13 @@ Qed.
 Lemma surj_equiv_alt : surjective f <-> incl fullset (Rg f).
 Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.
 
+Lemma surj_can_uniq_r :
+  forall {g h : T2 -> T1}, surjective f -> cancel f g -> cancel f h -> g = h.
+Proof.
+intros g h Hf Hg Hh; apply fun_ext; intros x2.
+destruct (Hf x2) as [x1 <-]; rewrite Hh; auto.
+Qed.
+
 End Range_Facts1.
 
 
@@ -333,13 +340,19 @@ Section Injective_Facts.
 
 Context {T1 T2 : Type}.
 Context {f : T1 -> T2}.
-Hypothesis Hf : injective f.
 
-Lemma inj_contra : forall x1 y1, x1 <> y1 -> f x1 <> f y1.
-Proof. move=>>; rewrite -contra_equiv; apply Hf. Qed.
+Lemma inj_contra : injective f -> forall x1 y1, x1 <> y1 -> f x1 <> f y1.
+Proof. intros Hf x1 y1; rewrite -contra_equiv; apply Hf. Qed.
+
+Lemma inj_contra_rev : (forall x1 y1, x1 <> y1 -> f x1 <> f y1) -> injective f.
+Proof. intros Hf x1 y1; rewrite contra_equiv; apply Hf. Qed.
+
+Lemma inj_contra_equiv :
+  injective f <-> forall x1 y1, x1 <> y1 -> f x1 <> f y1.
+Proof. split; [apply inj_contra | apply inj_contra_rev]. Qed.
 
-Lemma inj_equiv : forall x1 y1, f x1 = f y1 <-> x1 = y1.
-Proof. intros; split; [apply Hf | apply f_equal]. 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.
 
 End Injective_Facts.
 

FEM/Compl/Function_sub.v

@@ -114,6 +114,25 @@ Proof. move=>> H1 H2 x1 Hx1; rewrite H1// H2; easy. Qed.
 End Same_funS_Facts.
 
 
+Section RgS_Facts0.
+
+Context {T1 T2 : Type}.
+
+Variable P1 : T1 -> Prop.
+
+Variable f : T1 -> T2.
+
+Lemma imS_dec :
+  forall x2, { x1 | P1 x1 /\ f x1 = x2 } + { forall x1, P1 x1 -> f x1 <> x2 }.
+Proof.
+intros x2; destruct (in_dec (fun x2 => exists x1, P1 x1 /\ f x1 = x2) x2)
+    as [H1 | H1]; [left; apply ex_EX; easy | right; intros x1].
+rewrite imp_not_r_and_equiv; apply (not_ex_all_not _ _ H1).
+Qed.
+
+End RgS_Facts0.
+
+
 Section RgS_Facts1.
 
 Context {T1 T2 : Type}.
@@ -321,6 +340,20 @@ End FunS_Facts5.
 
 Section InjS_Facts1.
 
+Context {T : Type}.
+
+Context {P : T -> Prop}.
+
+Context {f : T -> T}.
+
+Lemma injS_id : same_funS P f (id : T -> T) -> injS P f.
+Proof. intros Hf x y Hx Hy; rewrite !Hf; easy. Qed.
+
+End InjS_Facts1.
+
+
+Section InjS_Facts2.
+
 Context {T1 T2 : Type}.
 
 Context {P1 : T1 -> Prop}.
@@ -331,22 +364,61 @@ Context {g : T1 -> T2}.
 Lemma injS_ext : same_funS P1 f g -> injS P1 f -> injS P1 g.
 Proof. intros Hg Hf x1 y1 Hx1 Hy1; rewrite -!Hg; auto. Qed.
 
-End InjS_Facts1.
+End InjS_Facts2.
 
 
-Section InjS_Facts2.
+Section InjS_Facts3.
 
 Context {T1 T2 : Type}.
 
+Context {P1 : T1 -> Prop}.
+
 Context {f : T1 -> T2}.
 
+Lemma injS_contra :
+  injS P1 f -> forall x1 y1, P1 x1 -> P1 y1 -> x1 <> y1 -> f x1 <> f y1.
+Proof. intros Hf x1 y1 Hx1 Hy1; rewrite -contra_equiv; auto. Qed.
+
+Lemma injS_contra_rev :
+  (forall x1 y1, P1 x1 -> P1 y1 -> x1 <> y1 -> f x1 <> f y1) -> injS P1 f.
+Proof. intros Hf x1 y1 Hx1 Hy1; rewrite contra_equiv; auto. Qed.
+
+Lemma injS_contra_equiv :
+  injS P1 f <-> forall x1 y1, P1 x1 -> P1 y1 -> x1 <> y1 -> f x1 <> f y1.
+Proof. split; [apply injS_contra | apply injS_contra_rev]. Qed.
+
+Lemma injS_equiv :
+  injS P1 f -> forall x1 y1, P1 x1 -> P1 y1 -> f x1 = f y1 <-> x1 = y1.
+Proof. intros; split; [auto | intro; subst; easy]. Qed.
+
 Lemma inj_S_equiv : injective f <-> injS fullset f.
 Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed.
 
-End InjS_Facts2.
+End InjS_Facts3.
 
 
-Section InjS_Facts3.
+Section InjS_Facts4.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+Context {g h : T2 -> T1}.
+
+Lemma injS_canS_uniq_l :
+  injS P1 f -> funS P2 P1 g -> funS P2 P1 h ->
+  canS P2 g f -> canS P2 h f -> same_funS P2 g h.
+Proof.
+intros H1 H2 H3 H4 H5 x2 Hx2; apply H1; [..| rewrite H5; auto];
+    [apply H2 | apply H3]; easy.
+Qed.
+
+End InjS_Facts4.
+
+
+Section InjS_Facts5.
 
 Context {T1 T2 T3 : Type}.
 
@@ -362,10 +434,10 @@ Proof.
 intros Hf0 Hf Hg x1 y1 Hx1 Hy1 H1; apply Hf, Hg; try apply Hf0; easy.
 Qed.
 
-End InjS_Facts3.
+End InjS_Facts5.
 
 
-Section InjS_Facts4.
+Section InjS_Facts6.
 
 Context {T1 T2 T3 : Type}.
 
@@ -379,7 +451,27 @@ Proof.
 intros H x1 y1 Hx1 Hy1 H1; apply H; try rewrite comp_correct H1; easy.
 Qed.
 
-End InjS_Facts4.
+End InjS_Facts6.
+
+
+Section InjS_Facts7.
+
+Context {T1 T2 T3 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Variable P2 : T2 -> Prop.
+
+Context {g h : T1 -> T2}.
+Context {f : T2 -> T3}.
+
+Lemma comp_injS_r :
+  funS P1 P2 g -> funS P1 P2 h -> injS P2 f ->
+  same_funS P1 (f \o g) (f \o h) -> same_funS P1 g h.
+Proof.
+move=> Hg Hh Hf H x1 Hx1; apply Hf, H; [apply Hg | apply Hh |]; easy.
+Qed.
+
+End InjS_Facts7.
 
 
 Section SurjS_Facts1.
@@ -468,6 +560,25 @@ End SurjS_Facts4.
 
 Section SurjS_Facts5.
 
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+Context {g h : T2 -> T1}.
+
+Lemma surjS_canS_uniq_r :
+  surjS P1 P2 f -> canS P1 f g -> canS P1 f h -> same_funS P2 g h.
+Proof.
+intros H1 H2 H3 x2 Hx2; destruct (H1 _ Hx2) as [x1 [Hx1 <-]]; rewrite H3; auto.
+Qed.
+
+End SurjS_Facts5.
+
+
+Section SurjS_Facts6.
+
 Context {T1 T2 T3 : Type}.
 
 Context {P1 : T1 -> Prop}.
@@ -553,10 +664,22 @@ Context {T1 T2 : Type}.
 Context {P1 : T1 -> Prop}.
 
 Context {f : T1 -> T2}.
-Variable g : T2 -> T1.
 
-Lemma canS_injS : canS P1 f g -> injS P1 f.
-Proof. move=> H x1 y1 Hx1 Hy1 /(f_equal g); rewrite !H; easy. Qed.
+Lemma canS_injS : forall (g : T2 -> T1), canS P1 f g -> injS P1 f.
+Proof. move=> g H x1 y1 Hx1 Hy1 /(f_equal g); rewrite !H; easy. Qed.
+
+Lemma injS_has_left_inv : inhabited T1 -> injS P1 f <-> exists g, canS P1 f g.
+Proof.
+intros [a1]; split; [intros Hf | intros [g Hg]; apply (canS_injS g), Hg].
+exists (fun x2 => match imS_dec P1 f x2 with
+  | inleft H1 => proj1_sig H1
+  | inright _ => a1
+  end).
+intros y1 Hy1; destruct (imS_dec P1 f (f y1)) as [[x1 [Hx1 H1]] | H1].
+simpl; apply Hf; easy.
+contradict H1; rewrite not_all_ex_not_equiv;
+    exists y1; rewrite not_imp_not_r_and_equiv; easy.
+Qed.
 
 End CanS_Facts3.
 
@@ -855,17 +978,11 @@ Context {g h : T2 -> T1}.
 Lemma bijS_canS_uniq_l :
   bijS P1 P2 f -> funS P2 P1 g -> funS P2 P1 h ->
   canS P2 g f -> canS P2 h f -> same_funS P2 g h.
-Proof.
-intros H1 H2 H3 H4 H5 x2 Hx2; apply (bijS_injS _ H1); [..| rewrite H5; auto];
-    [apply H2 | apply H3]; easy.
-Qed.
+Proof. move=> /bijS_injS; apply injS_canS_uniq_l. Qed.
 
 Lemma bijS_canS_uniq_r :
   bijS P1 P2 f -> canS P1 f g -> canS P1 f h -> same_funS P2 g h.
-Proof.
-move=> [f1 [_ [/funS_rev H1 [_ H2]]]] H3 H4 x2 Hx2; specialize (H1 _ Hx2).
-rewrite -(H2 _ Hx2) H3// H4; easy.
-Qed.
+Proof. move=> /bijS_surjS; apply surjS_canS_uniq_r. Qed.
 
 End BijS_Facts9.
 

FEM/Compl/logic_compl.v

@@ -78,18 +78,42 @@ Proof. tauto. Qed.
 Lemma not_or_equiv : ~ (P \/ Q) <-> ~ P /\ ~ Q.
 Proof. tauto. Qed.
 
+Lemma imp_and_equiv : (P -> Q) <-> ~ (P /\ ~ Q).
+Proof. tauto. Qed.
+
+Lemma imp_not_l_and_equiv : (~ P -> Q) <-> ~ (~ P /\ ~ Q).
+Proof. tauto. Qed.
+
+Lemma imp_not_r_and_equiv : (P -> ~ Q) <-> ~ (P /\ Q).
+Proof. tauto. Qed.
+
 Lemma imp_or_equiv : (P -> Q) <-> ~ P \/ Q.
 Proof. tauto. Qed.
 
-Lemma imp_and_equiv : (P -> Q) <-> ~ (P /\ ~ Q).
+Lemma imp_not_l_or_equiv : (~ P -> Q) <-> P \/ Q.
+Proof. tauto. Qed.
+
+Lemma imp_not_r_or_equiv : (P -> ~ Q) <-> ~ P \/ ~ Q.
 Proof. tauto. Qed.
 
 Lemma not_imp_and_equiv : ~ (P -> Q) <-> P /\ ~ Q.
 Proof. tauto. Qed.
 
+Lemma not_imp_not_l_and_equiv : ~ (~ P -> Q) <-> ~ P /\ ~ Q.
+Proof. tauto. Qed.
+
+Lemma not_imp_not_r_and_equiv : ~ (P -> ~ Q) <-> P /\ Q.
+Proof. tauto. Qed.
+
 Lemma not_imp_or_equiv : ~ (P -> Q) <-> ~ (~ P \/ Q).
 Proof. tauto. Qed.
 
+Lemma not_imp_not_l_or_equiv : ~ (~ P -> Q) <-> ~ (P \/ Q).
+Proof. tauto. Qed.
+
+Lemma not_imp_not_r_or_equiv : ~ (P -> ~ Q) <-> ~ (~ P \/ ~ Q).
+Proof. tauto. Qed.
+
 Lemma contra_equiv : (P -> Q) <-> (~ Q -> ~ P).
 Proof. tauto. Qed.