(** ** Bourbaki Sets 1 Exercices*)

Require Export set2.
Require Export set3.
Require Export set4.
Set Implicit Arguments.
(* $Id: sete1.v,v 1.39 2010/08/02 07:30:56 grimm Exp $ *)

Import Correspondence.
Import Bfunction.

Module Exercice1.

Lemma not_collectivizing_notin: 
  ~ (exists z, forall y, inc y z = not (inc y y)).
Proof. red. ir. nin H.
  assert (~ inc x x). red. ir. 
     cp H0. rwi (H x) H0. contradiction. 
  cp H0. wri (H x) H0. contradiction.
Qed.


Lemma collectivizing_special :
  (exists x, forall y, ~ (inc y x)) &  ~ (exists x, forall y, inc y x).
Proof. split. 
  exists emptyset. ir. red. app emptyset_pr. 
  red. ir. nin H. app not_collectivizing_notin.
    exists (Zo x (fun z => ~ (inc z z))). ir. app iff_eq; ir; Ztac; tv.
Qed. 

Lemma emptyset_pra: forall x (p: EP),
  inc x emptyset -> (p x).
Proof. ir.  elim (emptyset_pr H).
Qed.

Section exercise1_1.
Variable x y:Set.

Lemma exercise1_1: (x=y) = (forall X, inc x X -> inc y X).
Proof. ir. ap iff_eq; ir. ue. sy; ap singleton_eq; ap H; fprops.
Qed.

End exercise1_1.

Lemma exercise1_2: exists x:Set, exists y:Set, x <> y.
Proof. 
  assert (H:forall x:Set, emptyset <> singleton x). 
    red. ir. empty_tac1 (x).
  exists emptyset. exists (singleton emptyset). ap H.
Qed.

Lemma exercise1_3: forall X A B, sub A X -> sub B X ->
  (sub (complement X B) A = sub (complement X A) B     & 
  sub B (complement X A) = sub A (complement X B)).
Proof. intro X. assert (Ha:forall a b,  sub a X -> sub b X ->
    sub (complement X b) a -> sub (complement X a) b).
  ir. red. ir. srwi H2. ex_middle. nin H2. elim H4. app H1. srw. au. 
  assert (Hb: forall a b,  sub a X -> sub b X ->
    (sub (complement X b) a = sub (complement X a) b)). 
  ir. ap iff_eq; app Ha. split. app Hb. 
  cp (Hb _ _ (sub_complement (a:=X) (b:= A))(sub_complement (a:=X) (b:= B))). 
  srwi H1. am. am. am.
Qed.

Lemma exercise1_4: forall X x, 
  sub X (singleton x) = (X = singleton x \/ X = emptyset).
Proof. ir. ap iff_eq. ir.
  nin (p_or_not_p (sub (singleton x) X)); ir;
    [ left; app extensionality | right ]. 
  app is_emptyset. ir. dneg. red. ir. set (H _ H1). awi i; awi H2. ue. ue.
  ir. nin H; rw H; [ ap sub_refl | ap emptyset_sub_any]. 
Qed.

Lemma exercise1_5:
  emptyset = choose (fun X => ~ (inc (rep X) X)).
Proof.
  assert (forall Y y, inc y Y -> inc (rep Y) Y).
  ir. uf rep. app choose_pr. exists y. am.
  assert (forall Y,  ~ (inc (rep Y) Y) -> emptyset = Y).
  ir. sy. ap is_emptyset. ir. dneg. app (H _ _ H1).
  app H0. ap choose_pr. exists emptyset. red. ir. elim (emptyset_pr H1).
Qed.

Lemma exercise1_6:
  (forall y, y = choose (fun x => (forall z, (inc z x)=(inc z y)))) 
  -> (forall a b : Set, sub a b -> sub b a -> a = b).
Proof. ir. rw (H a). rw (H b). ufi sub H0.  ufi sub H1. 
  app choose_equiv. ir.  split. ir. rw H2. app iff_eq; au.
  ir. rw H2. app iff_eq; au.
Qed.


Lemma exercise2_1: forall R:EEP,
  (  (exists x, exists y, R x y) = (exists z, is_pair z & R(P z) (Q z)) &
     (forall x, forall y, R x y)  = (forall z, is_pair z -> R(P z) (Q z))).
Proof. ir. split;ap iff_eq;ir.
  nin H; nin H. exists (J x x0). split. fprops. aw. 
  destruct H as [x [H1 H2]]. exists (P x). exists (Q x). am.
  ap H. 
  assert (is_pair (J x y)). fprops. cp (H _ H0). awi H1. am.
Qed.

Definition xpair (x y : Set) :=
  doubleton (singleton x) (doubleton x (singleton y)).

Lemma exercise2_2 : forall x y z w, 
  (xpair x y = xpair z w) = (x = z & y = w).
Proof. ir. ap iff_eq; ir. 
  assert (inc (singleton x) (xpair z w)). wr H. uf xpair. fprops. 
  assert (inc (doubleton x (singleton y)) (xpair z w)). wr H. uf xpair. fprops.
  assert (x=z). nin (doubleton_or H0). app singleton_inj. 
  sy. app singleton_eq.  ue. 
  split. am. 
  wri H2 H1. nin (doubleton_or H1).
  assert (singleton y = x).  ap singleton_eq. ue.
  assert (inc (doubleton x (singleton w)) (xpair x y)). 
  rw H. rw H2. uf xpair. fprops. ufi xpair H5. rwi H4 H5.
  do 2 rwi doubleton_singleton H5. cp (singleton_eq H5).
  assert (singleton w = x). app singleton_eq. ue.
  app singleton_inj. ue.
  assert (inc (singleton w)  (doubleton x (singleton y))). ue.
  induction (doubleton_or H4). 
  assert (inc (singleton y)  (doubleton x (singleton w))). ue.
  induction (doubleton_or H6). 
  wri H5 H7; app singleton_inj. app singleton_inj.  sy;app singleton_inj.  
  nin H. ue. ue. 
Qed.

(* Definition has_no_graph (r:EEP):=
   ~(exists G, is_graph G & forall x y, r x y <-> inc (J x y) G). *)
Definition has_no_graph (r:EEP):=
 ~(exists G, forall x y, r x y -> inc (J x y) G).
Definition is_universal (r:EEP):= forall x, exists y, r x y \/ r y x.

Lemma is_universal_pr: forall r,  is_universal r -> has_no_graph r.
Proof. ir. red. red. ir. destruct H0 as [X H0].  
  nin collectivizing_special. elim H2. 
  exists (union2 (domain X)(range X)).
  ir. uf domain. uf range.
  nin (H y). nin H3. app union2_first. aw. exists (J y x). split. app H0. aw.
  app union2_second. aw. exists (J x y). split. app H0. aw.
Qed.

Lemma exercise3_1:
  has_no_graph (fun x y => inc x y) & 
  has_no_graph (fun x y => sub x y) & 
  has_no_graph (fun x y => x = singleton y).
Proof. eee; app is_universal_pr; red; ir ;
  [ exists (singleton x) | exists x |  exists (singleton x) ] ; fprops.
Qed.

Lemma exercise3_2: forall G X, is_graph G ->
  sub X (domain G) = 
  sub X (image_by_graph (inverse_graph G) (image_by_graph G X)).
Proof. ir. assert (Ha:is_graph (inverse_graph G)).  fprops. 
  ap iff_eq; ir; red; ir; pose (H0 _ H1); awi i; nin i.
  aw. exists x0. split. aw.  ex_tac. aw. am.
  nin H2; awii H3; ex_tac.
Qed. 

Lemma exercise3_3a: forall G H, is_graph G -> is_graph H ->
  sub (domain H) (domain G) =
  sub H (compose_graph H (compose_graph (inverse_graph G) G)).
Proof. ir. 
  app iff_eq. ir. red. ir. assert (Hp:= H1 _ H3).
  wri (pair_recov Hp) H3.
  assert (inc (P x) (domain G)). app H2. ex_tac.
  awi H4. induction H4.
  aw. split. am. ex_tac. aw. split. fprops. ex_tac.  aw.  am.
  ir. red. ir. awi H3. nin H3. cp (H2 _ H3). awi H4. nin H4. nin H5. nin H5.
  awi H5. nin H5. nin H7. nin H7. ex_tac. am. 
Qed.

Lemma exercise3_3b: forall G, is_graph G ->
  sub G (compose_graph G (compose_graph (inverse_graph G) G)).
Proof. ir. wr (exercise3_3a H H).  fprops. Qed.


Lemma exercise3_4a: forall G, 
  (compose_graph G emptyset = emptyset &
   compose_graph emptyset G = emptyset).
Proof. ir.  split.
  empty_tac. awi H. destruct H as [_ [z [H1 _ ]]]. elim (emptyset_pr H1). 
  empty_tac. awi H. destruct H as [_ [z [_ H1 ]]]. elim (emptyset_pr H1). 
Qed.


Lemma exercise3_4b: forall G, is_graph G ->
  (compose_graph (inverse_graph G) G = emptyset) = (G = emptyset).
Proof. ir. 
  app iff_eq. ir. empty_tac. empty_tac1  (J (P y) (P y)).
  aw. split. fprops. set (H _ H1). exists (Q y). split; aw.  
  ir. rw H0. nin (exercise3_4a (inverse_graph emptyset)). am.
Qed.

Lemma exercise3_5: forall G A B, 
  (compose_graph (product A B) G = product (inv_image_by_graph G A) B &
  compose_graph G (product A B)  = product A (image_by_graph G B)).
Proof. ir.  
  split; set_extens; awii H.
  destruct H as [H1 [y [H2 H3]]]. awi H3. ee. aw. eee. ex_tac. 
  destruct H as [H1 [ [y [H2 H3]] H4]]. aw. eee. ex_tac. fprops.
  destruct H as [H1 [y [H2 H3]]]. awi H2. aw. eee. ex_tac. 
  destruct H as [H1 [ H2 [y [H3 H4]]]]. aw. eee. ex_tac. fprops. 
Qed.

Definition complement_graph G :=
  complement(product (domain G) (range G)) G.

Lemma complement_graph_g : forall G, is_graph (complement_graph G).
Proof. red. uf complement_graph.  ir. srwi H. nin H.
  rwi product_inc_rw H. nin H; am. 
Qed.

Lemma exercise3_6a: forall G, is_graph G ->
  complement_graph (inverse_graph G) = inverse_graph(complement_graph G).
Proof. ir.  assert (Ha: is_graph (complement_graph G)). ap complement_graph_g.
  uf complement_graph. bw. rww range_inverse.
  set (u:= range G) in *. set (v:= domain G) in *. set_extens.
  srwi H0. nin H0. awi H0. rw inverse_graph_rw. eee. srw. split. aw. eee.
  nin H2. rwi inverse_graph_rw H2. awi H2. uf u. nin H2. ex_tac. am.
  dneg. rw inverse_graph_rw. au. am. am. fprops.
  rwi inverse_graph_rw H0. nin H0. srwi H1. nin H1. awii H1. ee.
  srw. split.  rw domain_inverse. fold u. aw;eee. am.
  rw inverse_graph_rw. dneg. nin H5. am.   am. am.
Qed. 

Lemma exercise3_6b: forall G B, is_graph G -> sub (range G) B ->
  sub (compose_graph G (complement_graph (inverse_graph G)))
      (complement_graph (identity_g B)).
Proof. ir. rww  exercise3_6a.  red. 
  uf complement_graph. ir. srw.
  rw identity_domain. rw identity_range. rw inc_diagonal_rw.
  awi H1. destruct H1 as [H2 [y [ H3 H4]]]. awi H3. srwi H3. nin H3.
  split. aw. eee. app H0. set (u:=range G) in *. awi H1. eee. am.
  app H0. ex_tac. dneg. eee. 
Qed.

Lemma exercise3_6c: forall A G, is_graph G -> sub (domain G) A ->
  sub (compose_graph (complement_graph (inverse_graph G)) G)
      (complement_graph (identity_g A)).
Proof. ir. red. rww exercise3_6a. uf complement_graph.
  rw identity_domain. rw identity_range. ir. srw. rw inc_diagonal_rw. 
  awi H1. destruct H1 as [H2 [y [ H3 H4]]]. awi H4. srwi H4. nin H4.
  split. aw. eee. app H0. ex_tac. app H0.
  set (u:=domain G) in *. awi H1. eee. am. dneg.  eee. 
Qed.

Lemma exercise3_6d: forall G, is_graph G ->
  ( G = product (domain G)(range G) ) = 
  (compose_graph G (compose_graph (complement_graph (inverse_graph G)) G)
  = emptyset ).
Proof. ir.  rw (exercise3_6a H). set (K:= complement_graph G).
  assert(Ha: (G = product (domain G) (range G)) = (K = emptyset)).
  uf K. uf complement_graph. ap iff_eq. ir. wr H0. app complement_itself. 
  ir. ap extensionality. app sub_graph_prod. app empty_complement.
  rw Ha. 
  app iff_eq. ir. rw H0. rw inverse_graph_emptyset.
  nin (exercise3_4a G). rw H2. rw H1. tv.
  ir. ap is_emptyset. red. ir. cp H1.
  ufi K H1. ufi complement_graph H1. srwi H1. nin H1. awii H1. ee.
  nin H4; nin H5.
  elim (emptyset_pr (x:=(J x0 x))).  wr H0. aw. eee. 
  ex_tac. aw. eee. ex_tac. aw. 
Qed.

Lemma exercise3_7: forall G, is_graph G ->
  fgraph G = (forall X, sub (image_by_graph G (inv_image_by_graph G X)) X).
Proof. ir.
  uf inv_image_by_graph. ap iff_eq. ir. red. ir. awi H1. nin H1.
  nin H1. awi H1.  nin H1. nin H1. awi H3. 
  red in H0. nin H0. assert (P (J x0 x1) = P (J x0 x)). aw.
  cp (H4 _ _ H3 H2 H5).  wrr (pr2_def H6). 
  ir. red. split. am. ir. cp (H _ H1). cp (H _ H2). 
  app pair_extensionality. 
  app singleton_eq. app (H0 (singleton (Q y))). aw. exists (P x). split.
  aw. exists (Q y).  split.  fprops. aw. rw H3. aw. red.  aw.
Qed.  

Lemma exercise3_8: forall G G', is_correspondence G -> is_correspondence G' ->
  source G = target G' -> source G' = target G ->
  (forall x, inc x (source G) -> image_by_fun G' (image_by_fun G (singleton x))
    = singleton x) ->
  (forall x, inc x (source G') -> image_by_fun G (image_by_fun G' (singleton x))
    = singleton x) ->
  (bijective G & bijective G' & G = inverse_fun G').
Proof. ir. ufi image_by_fun H3. ufi image_by_fun H4.
  assert (Ha:is_graph (graph G)). fprops. 
  assert (Hb:is_graph (graph G')). fprops.
  assert (Hc:source G = domain (graph G)). app extensionality. red. ir.
  cp (H3 _ H5). assert (inc x (singleton x)). fprops. wri H6 H7.
  awi H7. nin H7. nin H7. awi H7. nin H7. nin H7. awi H7. rwi H7 H9.  
  set (aux:=graph G). ex_tac. fprops.
  assert (Hd:source G' = domain (graph G')). app extensionality. red. ir.
  cp (H4 _ H5). assert (inc x (singleton x)). fprops. wri H6 H7.
  awi H7. nin H7. nin H7. awi H7. nin H7. nin H7.  set (aux:=graph G'). aw. 
  wr (singleton_eq H7). ex_tac. fprops.
  assert (forall x y z, inc (J x y)(graph G) -> inc (J y z)(graph G') -> x = z).
  ir.  assert (inc x (source G)). rw Hc.   set (aux:=graph G). ex_tac. 
  sy. ap singleton_eq. wr (H3 _ H7). aw. ex_tac. aw. ex_tac. fprops.
  assert (forall x y z, inc (J x y)(graph G') -> inc (J y z)(graph G) -> x = z).
  ir.  assert (inc x (source G')). rw Hd.   set (aux:=graph G').  ex_tac.
  sy. ap singleton_eq. wr (H4 _ H8). aw. ex_tac. aw. ex_tac. fprops.
  assert (forall x, inc x (source G) -> exists y,
    inc (J x y) (graph G) & inc (J y x) (graph G')).
  ir. cp (H3 _ H7). assert (inc x (singleton x)). fprops. wri H8 H9. 
  awi H9.  nin H9. nin H9.  awi H9.  nin H9. nin H9. 
  rwi (singleton_eq H9) H11.  ex_tac. 
  assert (forall x, inc x (source G') -> exists y,
    inc (J x y) (graph G') & inc (J y x) (graph G)).
  ir. cp (H4 _ H8). assert (inc x (singleton x)). fprops. wri H9 H10. 
  awi H10.  nin H10. nin H10.  awi H10.  nin H10. nin H10. 
  rwi (singleton_eq H10) H12.  ex_tac.
  assert (fgraph (graph G)). red. split. am. ir.
  assert (is_pair x). app Ha. assert (J (P x) (Q x) = x). aw.
  wri H13 H9. 
  assert (inc (P x) (source G)). rw Hc.  set (aux:=graph G). ex_tac. 
  cp (H7 _ H14). nin H15. nin H15. cp  (H6 _ _ _ H16 H9).
  assert (is_pair y). app Ha. assert (J (P y) (Q y) = y). aw.
  wri H19 H10. wri H11 H10. cp  (H6 _ _ _ H16 H10).
  wr H13; wr H19; wr H17; wr H20; wr H11; tv.
  assert (fgraph (graph G')). red. split. am. ir.
  assert (is_pair x). app Hb. assert (J (P x) (Q x) = x). aw.
  wri H14 H10. assert (inc (P x) (source G')). rw Hd.   
  set (aux:=graph G'). ex_tac.
  cp (H8 _ H15). nin H16. nin H16. cp  (H5 _ _ _ H17 H10).
  assert (is_pair y). app Hb. assert (J (P y) (Q y) = y). aw.
  wri H20 H11. wri H12 H11. cp  (H5 _ _ _ H17 H11).
  wr H14; wr H20; wr H18; wr H21; wr H12; tv.
  assert(is_function G). red. intuition.
  assert(is_function G'). red. intuition.
  assert (graph G = inverse_graph(graph G')). set_extens.
  assert (is_pair x). app Ha. assert (J (P x) (Q x) = x). aw.
  wr H15. wri H15 H13. aw. assert (inc (P x) (source G)). rw Hc.   
  set (aux:=graph G). ex_tac.
  cp (H7 _ H16). nin H17.  nin H17. cp (H6 _ _ _ H18 H13). ue.
  assert (is_pair x). assert (is_graph (inverse_graph (graph G'))).
  ap inverse_graph_is_graph. app H14. assert (J (P x) (Q x) = x). aw.
  wri H15 H13. awi H13.  wr H15.
  assert (inc (P x) (source G)). rw H1. app corresp_sub_range. aw.
  ex_tac.  cp (H7 _ H16). nin H17.  nin H17. cp (H6 _ _ _ H13 H17). ue.
  assert(G = inverse_fun G'). uf inverse_fun. wr H1. rw H2. wr H13. sy.
  app corresp_recov. nin H11; nin H11; am.
  assert (bijective G). red. split. red. split. am. ir. 
  cp (W_pr3 H11 H15). assert (inc (W x G) (source G')). rw H2.  fprops.
  cp (H8 _ H19). nin H20. nin H20. cp (H5 _ _ _ H18 H20).
  rwi H17 H20.  cp (W_pr3 H11 H16). cp (H5 _ _ _ H23 H20). rww H24.
  ap surjective_pr5. am. ir. wri H2 H15. cp (H8 _ H15). nin H16.
  nin  H16. uf related. ex_tac. rw Hc.   set (aux:=graph G). aw. ex_tac.
  split. am. split. assert (G' = inverse_fun G). rw H14.
  rw inverse_fun_involutive. tv. am. rw H16. app inverse_bij_is_bij1. am.
Qed.

Lemma exercise3_9: forall  f g h,
  is_function f -> is_function g -> is_function h->
  source g = target f -> source h = target g ->
  bijective(compose g f) -> bijective (compose h g) ->
  (bijective f & bijective g & bijective h).
Proof. ir. assert (composable g f). red. intuition. 
  assert (composable h g). red. intuition. 
  assert(injective g). red in H5; nin H5.  app (inj_right_compose H7 H5).
  assert(surjective g). red in H4; nin H4.  app (surj_left_compose H6 H9).
  assert (bijective g). red. intuition. split. 
  app (bij_right_compose H6 H4 H10). split. am.
  app (bij_left_compose H7 H5 H10). 
Qed.

Lemma exercise3_10: forall  f g h,
  is_function f -> is_function g -> is_function h->
  source g = target f -> source h = target g ->  source f = target h ->
  injective (compose h (compose g f)) ->
  surjective (compose g (compose f h)) ->
  (injective (compose f (compose h  g)) 
   \/ surjective (compose f (compose h  g))) ->
  (bijective f & bijective g & bijective h).
Proof. ir. 
  assert (composable f h). red. au.
  assert (composable h g). red. au.
  assert (composable g f). red; au.
  wri compose_assoc H5; try am.
  assert (is_function (compose h g)).  fct_tac.
  assert (composable (compose h g) f). red. aw.  au.
  cp (inj_right_compose H12 H5).
  assert (is_function (compose f h)). fct_tac.
  assert (composable g (compose f h)). red. aw. au.
  cp (surj_left_compose H15 H6).
  nin H7.
  wri compose_assoc H7; try am. 
  assert (composable (compose f h) g). red. aw. au.
  cp (inj_right_compose H17 H7).
  cp (surj_left_compose2 H15 H6 H18). 
  cp (surj_left_compose H8 H19). 
  cp (inj_left_compose2 H17 H7 H16). 
  assert (bijective (compose f h)). red. aw. au.
  assert (bijective f). red. au.  
  ee. am. split;am. app (bij_right_compose H8 H22 H23).
  assert (composable f (compose h g)). red. aw. au.
  cp (surj_left_compose H17 H7).
  cp (surj_left_compose2 H17 H7 H13). 
  cp (inj_left_compose2 H12 H5 H18).
  cp (inj_right_compose H9 H20). assert (bijective g). red; au.
  ee. red; au. am. 
  assert (bijective (compose h g)). red. aw. au.
  app (bij_left_compose H9 H23 H22).
Qed.

Lemma exercise4_1a: forall g,  is_graph g  ->
  functional_graph g = (forall x y, inv_image_by_graph g (intersection2 x y)=
    intersection2 (inv_image_by_graph g x) (inv_image_by_graph g y)).
Proof. ir. assert (is_graph (inverse_graph g)).  fprops. 
  uf inv_image_by_graph. app iff_eq. ir. set_extens. awi H2.
  nin H2. nin H2. app intersection2_inc; aw; ex_tac; inter2tac.
  nin (intersection2_both H2). awi H3. awi H4.
  nin H3; nin H4. nin H3; nin H4. awi H5.  awi H6.
  cp (H1 _ _ _ H5 H6). aw. exists x1. split.
  app intersection2_inc. rww H7. aw. 

  ir. red. ir. cp (H1 (singleton y)(singleton y')).  
  set (u:=intersection2 (singleton y) (singleton y')). 
  assert (inc x (image_by_graph (inverse_graph g) u)). uf u. rw H4.
  app intersection2_inc. aw. ex_tac. aw. aw. ex_tac. aw.
  awi H5. nin H5. nin H5. ufi u H5. nin (intersection2_both H5). 
  awi H7. awi H8. ue. 
Qed.

Lemma exercise4_1b: forall g,  is_graph g  ->
  functional_graph g = (forall x y, intersection2 x y = emptyset ->
    intersection2 (inv_image_by_graph g x) (inv_image_by_graph g y)=emptyset).
Proof. ir. app iff_eq. ir. rwi exercise4_1a H0. wr H0. rw H1. 
  uf inv_image_by_graph. rww image_by_emptyset. am.
  ir. red. ir. assert (is_graph (inverse_graph g)). fprops.
  set (v:= intersection2 (image_by_graph (inverse_graph g) (singleton y))
         (image_by_graph (inverse_graph g) (singleton y'))).
  assert (inc x v). uf v. app intersection2_inc. aw. ex_tac.
  aw. aw. ex_tac. aw.
  nin (emptyset_dichot (intersection2 (singleton y) (singleton y'))).
  cp (H0 _ _ H5). assert (inc x emptyset). wr H6. am.
  elim (emptyset_pr H7). nin H5. 
  nin (intersection2_both H5). awi H6. awi H7. ue. 
Qed.

Lemma exercise4_2a: forall g x,  is_graph g  ->
  image_by_graph g x = range(intersection2 g (product x (range g))).
Proof. ir. assert(is_graph (intersection2 g (product x (range g)))).
  red. ir. app H. inter2tac.
  set_extens. awi H1. nin H1. nin H1. aw. exists x1. 
  app intersection2_inc. aw. eee. ex_tac.
  awi H1. nin H1. nin (intersection2_both H1). 
  aw. ex_tac. awi H3. ee. am. am. am. 
Qed.

Lemma exercise4_2b: forall g x,  is_graph g  ->
  image_by_graph g x = image_by_graph g (intersection2 x (domain g)).
Proof. ir. set_extens. awi H0. nin H0. nin H0. aw. exists x1. split. 
  app intersection2_inc. ex_tac. am. 
  awi H0. nin H0. nin H0. aw. ex_tac. inter2tac.
Qed.

Lemma exercise4_3a: forall  x y y' z, intersection2 y y' = emptyset ->
  compose_graph(product y' z)(product x y) = emptyset.
Proof. ir.  app is_emptyset. ir. red. ir. awi H0.  
  nin H0. nin H1. nin H1. awi H1. awi H2. ee.
  elim (emptyset_pr (x:=x0)).  wr H. app intersection2_inc. 
Qed.
Lemma exercise4_3b: forall  x y y' z, nonempty(intersection2 y y') ->
  compose_graph(product y' z)(product x y) = product x z.
Proof. ir.  nin H. set_extens. awi H0. nin H0. nin H1. nin H1. awi H1; awi H2.
  aw. eee.
  awi H0. ee. nin (intersection2_both H). aw. split. am. exists y0. fprops. 
Qed.

Lemma exercise4_4a:  forall g x,
  image_by_graph(unionb g) x = 
  unionb (L(domain g) (fun i=> image_by_graph(V i g) x)).
Proof. ir.
  set_extens. awi H. nin H. nin H. rwi unionb_rw H0.
  nin H0. nin H0. apply unionb_inc with x2. bw. bw. aw.  ex_tac.
  rwi unionb_rw H. nin H. nin H. bwi H.  bwi H0. awi H0. nin H0.
  nin H0. aw. ex_tac. apply unionb_inc with x1. am. am. am.
Qed.


Lemma exercise4_4b:  forall g x,
  nonempty g -> is_singleton x ->
  image_by_graph(intersectionb g) x = 
  intersectionb (L(domain g) (fun i=> image_by_graph(V i g) x)).
Proof. ir.
  red in H0. nin H0. rw H0.
  assert (Hb:nonempty
    (L (domain g) (fun i => image_by_graph (V i g) (singleton x0)))).
  assert (exists y, inc y (domain g)). nin H. exists (P y). uf domain.
  aw. ex_tac. nin H1. rename x1 into y.
  set (ff:=  (fun i=> image_by_graph (V i g) (singleton x0))).
  exists (J y (ff y)). uf L. aw. exists y. au.
  set_extens. awi H1. nin H1. nin H1. cp (singleton_eq H1). rwi H3 H2.
  rwi intersectionb_rw H2.
  ap intersectionb_inc. am. bw. ir. bw. aw. ex_tac. rw H3. app H2. am.
  aw. ex_tac. apply intersectionb_inc. am. ir.
  rwi intersectionb_rw H1. bwi H1. cp (H1 _ H2). bwi H3. 
  awi H3. nin H3. nin H3. rwi (singleton_eq H3) H4. am. am. am.
Qed. 

Lemma exercise4_4c: 
  let x:=TPa in let y:= TPb in 
    let G:= doubleton(J x x)(J y y) in let H:=  doubleton(J x y)(J y x)
      in let z:= doubleton x y in
        image_by_graph (intersection2 G H) z <> 
        intersection2 (image_by_graph G z)(image_by_graph H z).
Proof. ir. assert (x <> y). app two_points_distinct. 
  assert (Ha:is_graph G). red. ir. nin (doubleton_or H1); rw H2; fprops. 
  assert (Hb:is_graph H). red. ir. nin (doubleton_or H1); rw H2; fprops. 
  assert (Hc:image_by_graph G z = z). set_extens. awi H1. nin H1. nin H1.
  nin (doubleton_or H2);  cp (pr2_def H3);rw H4; uf z; fprops.
  nin (doubleton_or H1); aw; ex_tac; rww H2; uf G; fprops.
  assert (Hd:image_by_graph H z = z). set_extens. awi H1. nin H1. nin H1.
  nin (doubleton_or H2);  cp (pr2_def H3); rw H4;  uf z; fprops.
  aw. uf H. nin (doubleton_or H1);  [ exists y | exists x] ; 
  rw H2; split; uf z;fprops;  uf H; fprops.
  assert (He: intersection2 G H = emptyset). app is_emptyset. red. ir.
  nin (intersection2_both H1). elim H0.
  nin (doubleton_or H2); nin (doubleton_or H3); rwi H4 H5; 
    try rw (pr2_def H5); try rw (pr1_def H5); au. 
  rw Hc. rw Hd. rw He. rw intersection2idem.
  assert (inc x z). uf z. fprops. red. ir. wri H2 H1. awi H1. nin H1. nin H1.
  red in H3. elim (emptyset_pr H3).
Qed.

Lemma exercise4_5: forall G H,
  (compose_graph (unionb G) H = 
     unionb (L(domain G) (fun i=> compose_graph(V i G) H))
     & compose_graph H (unionb G) = 
     unionb (L(domain G) (fun i=> compose_graph H (V i G)))).
Proof. ir. split.  
  set_extens. awi H0. nin H0. nin H1. nin H1. 
  rwi unionb_rw H2. nin H2. nin H2. apply unionb_inc with x1. bw. bw. aw.
  ee. am. ex_tac. 
  rwi unionb_rw H0. nin H0. nin H0. bwi H0. bwi H1. awi H1. nin H1. nin H2. 
  nin H2. aw. split. am. ex_tac.
  apply unionb_inc with x0;tv. am. 
  set_extens. awi H0. nin H0. nin H1. nin H1. 
  rwi unionb_rw H1. nin H1. nin H1. apply unionb_inc with x1. bw. bw. aw.
  ee. am. ex_tac.
  rwi unionb_rw H0. nin H0. nin H0.  bwi H0. bwi H1. awi H1. nin H1. nin H2. 
  nin H2. aw. split. am. ex_tac. apply unionb_inc with x0; am. am. 
Qed.

Lemma exercise4_6:  forall G, is_graph G ->
  fgraph G = (forall H H', is_graph H -> is_graph H' ->
    compose_graph (intersection2  H H') G = 
    intersection2 (compose_graph H G) (compose_graph H' G)).
Proof. ir.  app iff_eq. ir. 
  set_extens. awi H4. nin H4. nin H5. nin H5. 
  app intersection2_inc; aw; split; tv; ex_tac; inter2tac.
  nin (intersection2_both H4).
  awi H5; awi H6.  nin H5; nin H6. nin H7;nin H8. nin H7; nin H8.
  nin H0. assert (P (J (P x) x0) = P (J (P x) x1)). aw.  
  cp (H11 _ _ H7 H8 H12). cp (pr2_def H13).
  aw. split. am. ex_tac. app intersection2_inc. ue.

  ir. red. split. am. ir. 
  set (h:= singleton(J (Q x) (P x))).
  set (h':= singleton(J (Q y) (P y))). 
  assert (is_graph h). uf h. red. ir. db_tac.  
  assert (is_graph h'). uf h'. red. ir. db_tac.
  cp (H _ H1). wri (pair_recov H6) H1.
  cp (H _ H2). wri (pair_recov H7) H2.
  assert (inc (J (P x)(P x)) (compose_graph h G)). aw. split. fprops.
  ex_tac. uf h.  fprops.
  assert (inc (J (P y)(P y)) (compose_graph h' G)). aw. split. fprops.
  ex_tac. uf h'. fprops.
  assert (inc (J (P x)(P x)) (compose_graph (intersection2 h h') G)).
  rww H0. app intersection2_inc. rww H3. awi H10. nin H10. nin H11. nin H11.
  nin (intersection2_both H12). ufi h H13. cp (singleton_eq H13).
  ufi h H14. cp (singleton_eq H14).
  app pair_extensionality.  rwi H15 H16. inter2tac.
Qed. 

Lemma exercise4_7:  forall G H K, 
  sub(intersection2 (compose_graph H G) K) 
     (compose_graph(intersection2 H (compose_graph K (inverse_graph G)))
       (intersection2 G (compose_graph (inverse_graph H) K))).
Proof. ir. red. ir. nin (intersection2_both H0).
  awi H1. nin H1. nin H3. nin H3. assert (J (P x)(Q x)=x). aw.
  wri H5 H2. aw. split. am. exists x0. 
  split; inter2tac; aw; split;fprops; ex_tac; aw. 
Qed.


Lemma exercise4_8a:  forall dr r ds s x, 
  covering_f dr r x -> covering_f ds s x ->
  partition_fam (L ds s) x ->  coarser_covering ds s dr r ->
  (forall k, inc k ds -> nonempty (s k)) ->
  forall k, inc k ds -> exists i, inc i dr & sub (r i) (s k).
Proof. ir. red in H1. ee. cp (H3 _ H4). nin H7. assert (inc y x). wr H6.
  apply unionb_inc with k. bw. bw. red in H. assert (inc y (unionf dr r)).
  app H. nin (unionf_exists H9). nin H10. ex_tac.
  nin (H2 _ H10). nin H12. assert (inc y (s x1)). app H13.
  red in H5. bwi H5. nin (H5 _ _ H4 H12). ue.
  red in H15. elim (emptyset_pr (x:=y)).  wr H15. bw. app intersection2_inc. 
Qed.

Lemma exercise4_8b: let a:= TPa in let b:= TPb in 
  let x:= doubleton a b in let dr:= singleton a in let r:= fun _ => x
    in let ds:= x in let s:= variant a x (singleton a) in  
      (covering_f dr r x & covering_f ds s x &
        coarser_covering ds s dr r &
        (forall k, inc k ds -> nonempty (s k)) &
        ~ (forall k, inc k ds -> exists i, inc i dr & sub (r i) (s k))).
Proof. ir. uf ds; uf dr.
  assert (Ha: b<> a). uf a; uf b. app two_points_distinctb.
  split. red. red. ir. apply unionf_inc with a. fprops.
  uf r. am. split. red. red. ir. uf x. apply unionf_inc with a; fprops.
  uf s. rww variant_if_rw. 
  split. red. ir.  exists a. split. uf x. fprops.
  uf s. rww variant_if_rw. uf r. fprops. 
  split. ir. ufi x H. uf s. nin (doubleton_or H); rw H0.
  rww variant_if_rw. uf x. app nonempty_doubleton. 
  rww variant_if_not_rw. app nonempty_singleton.
  red. ir. assert (inc b x). uf x. fprops. nin (H _ H0). nin H1. 
  ufi r H2. ufi s H2. rwii variant_if_not_rw H2. cp (H2 _ H0). awi H3.
  contradiction.
Qed.

Inductive four_points : Set :=  | fpa  | fpb | fpc |  fpd.
Inductive three_points : Set :=  | tpa  | tpb | tpc.

Ltac disc:=
  match goal with 
    |- Ro ?x <> Ro ?y => 
      red; ir;cut(x = y); [ intros hyp; discriminate hyp | app  R_inj]
    | h:Ro ?x = Ro ?y |- False => 
     cut(x = y); [ intros hyp; discriminate hyp | app  R_inj]
end.
  

Lemma exercise4_8c:
  let x:= four_points in let dr:= three_points in
    let r:= fun i=>  Yo (i = (Ro tpa)) (singleton (Ro fpa))
      (Yo (i = (Ro tpc)) (singleton (Ro fpb)) (doubleton (Ro fpc) (Ro fpd)))
      in let ds:= doubleton(Ro fpa) (Ro fpb)
        in let s:= variant (Ro fpa) (doubleton (Ro fpa) (Ro fpc))
          (doubleton (Ro fpb) (Ro fpd))
          in (partition_fam (L ds s) x &
            partition_fam (L dr r) x&
           (forall k, inc k ds -> exists i, inc i dr & sub (r i) (s k))&
           ~( coarser_covering ds s dr r )).
Proof. ir. 
  assert (Hw: Ro fpb <> Ro fpa). disc. 
  split. red. split. gprops. split.
  assert (disjoint (V (Ro fpa) (L ds s)) (V (Ro fpb) (L ds s))).
  uf ds. bw. uf s. rww variant_if_rw. rw variant_if_not_rw. 
  app disjoint_pr. ir. nin (doubleton_or H);  nin (doubleton_or H0);
  rwi H1 H2; disc. exact Hw.
  fprops. fprops.
  red. bw. ir. nin (doubleton_or H0); nin (doubleton_or H1); rw H2; rw H3;
  solve [ left; tv | right; am | right; app disjoint_symmetric].

  uf ds. uf s. set_extens. nin (unionb_exists H); nin H0; bwi H0; bwi H1;
    nin (doubleton_or H0); rwi H2 H1. 
  rwii variant_if_rw H1. nin (doubleton_or H1);  rw H3; app R_inc.
  rwii variant_if_not_rw H1. nin (doubleton_or H1);  rw H3; app R_inc. am. am. 
  nin H. wr H. elim x1 ; 
   [ set (v:= fpa) | set (v:= fpb) | set (v:= fpa) |  set (v:= fpb) ];
   apply unionb_inc with (Ro v); bw; fprops; bw;
   solve [  rww variant_if_rw;  fprops; fprops |
            rww variant_if_not_rw; fprops; fprops ].

  assert (Ha:disjoint (r (Ro tpa)) (r (Ro tpb))).
  uf r. rww Y_if_rw. rww Y_if_not_rw. rww Y_if_not_rw.
  app disjoint_pr. ir. awi H.  rwi H H0.
  nin (doubleton_or H0); disc. disc. disc.
  assert (Hb:disjoint (r (Ro tpa)) (r (Ro tpc))).
  uf r. rww Y_if_rw.  rww Y_if_not_rw. rww Y_if_rw.
  app disjoint_pr. ir. awi H. awi H0. rwi H0 H.  disc. disc.
  assert (Hc:disjoint (r (Ro tpc))  (r (Ro tpb))).
  uf r. rww Y_if_not_rw. rww Y_if_rw.  rww Y_if_not_rw. rww Y_if_not_rw.
  app disjoint_pr. ir. awi H.  rwi H H0.
  nin (doubleton_or H0); disc. disc. disc. disc.
  split. red. split. gprops. split. 
  red. ir. bwi H. bwi H0. bw. ufi dr H.
  ufi dr H0.  nin H; nin H0. wr H; wr H0. elim x0; elim x1; 
   solve [ left; tv | right; am | right; app disjoint_symmetric].


  set_extens. nin (unionb_exists H). nin H0. bwi H0. bwi H1. ufi r H1. 
  ufi dr H0. nin H0. wri H0 H1. induction x2. rwii Y_if_rw H1. 
  rw (singleton_eq H1). app R_inc. rwi Y_if_not_rw H1. rwi Y_if_not_rw H1. 
  nin (doubleton_or H1);rw H2; app R_inc. disc. disc.
  rwi Y_if_not_rw H1. rwi Y_if_rw H1.  rw (singleton_eq H1). 
  app R_inc. tv.  disc. am. 
  uf r. nin H. wr H. 
  induction x1 ; [set (v:= tpa) | set (v := tpc) | set (v := tpb)
    | set (v:= tpb) ] ; apply unionb_inc with (Ro v); bw; try app R_inc.
  rww Y_if_rw. fprops. 
  rw Y_if_not_rw. rw Y_if_rw. fprops. tv. disc. 
  rw Y_if_not_rw. rw Y_if_not_rw. fprops. disc.  disc. 
  rw Y_if_not_rw. rw Y_if_not_rw. fprops. disc.  disc. 

  split. uf s. uf r.  ir. ufi ds H. nin (doubleton_or H). rw H0.
  rww variant_if_rw. exists (Ro tpa). split. app R_inc. 
  rww Y_if_rw.  red. ir. db_tac. 
  rw H0. rw variant_if_not_rw. exists (Ro tpc). split. app R_inc. 
  rw Y_if_not_rw. rww Y_if_rw. red. ir. db_tac. disc. disc.
  red. ir. red in H. induction (H _ (R_inc tpb)).  nin H0. ufi r H1. 
  rwi Y_if_not_rw H1. rwi Y_if_not_rw H1.
  assert (inc (Ro fpc) (s x0)). app H1. fprops.
  assert (inc (Ro fpd) (s x0)). app H1. fprops.
  ufi ds H0. nin (doubleton_or H0). rwi H4 H3. ufi s H3.
  rwi variant_if_rw H3. nin (doubleton_or H3);  disc. tv.
  rwi H4 H2. ufi s H2. rwi variant_if_not_rw H2. 
  nin (doubleton_or H2); disc. am. disc. disc.
Qed.



Lemma exercise5_f1: forall x y, sub(powerset x) (powerset y) -> sub x y.
Proof. ir. red. ir. assert (sub (singleton x0) y). app powerset_sub. app H.
  app powerset_inc. red. ir. db_tac. red in H1. 
  app (H1 x0). fprops.
Qed.

Lemma exercise5_f2: forall f x v w,
  is_function f -> source f = (powerset x) -> target f = powerset x ->
  (forall a b, inc a (powerset x) -> inc b (powerset x) -> sub a b 
    -> sub (W a f) (W b f)) ->
  v = intersection(Zo (powerset x) (fun z=> sub (W z f) z)) ->
  w = union(Zo (powerset x) (fun z=> sub z (W z f))) ->
  (W v f = v & W w f = w & (forall z, sub z x -> W z f = z ->
    (sub v z & sub z w))).
Proof. ir.
  set (q:= (Zo (powerset x) (fun z => sub (W z f) z))).
  assert (nonempty q). uf q. exists x. Ztac. app inc_x_powerset_x.
  app powerset_sub. wr H1. cp (inc_x_powerset_x x). wri H0 H5. fprops.
  set (p:= (Zo (powerset x) (fun z  => sub z (W z f)))).
  assert (Ha:forall z, sub z x -> W z f = z -> sub v z). ir.
  assert (inc z q). uf q. Ztac. app powerset_inc. rw H7. fprops. rw H3.
  fold q. app intersection_sub.
  assert (Hb:forall z, sub z x -> W z f = z -> sub z w). ir.
  assert (inc z p). uf p. Ztac. app powerset_inc. rw H7. fprops. rw H4.
  fold p. app union_sub.
  assert (Hc:forall z, inc z q -> inc (W z f) q). ir. ufi q H6. Ztac. clear H6.
  assert (inc (W z f) (powerset x)).  wr H1. wri H0 H7.  fprops. uf q. Ztac.
  assert (Hd:forall z, inc z p -> inc (W z f) p). ir. ufi p H6. Ztac. clear H6.
  assert (inc (W z f) (powerset x)).  wr H1. wri H0 H7.  fprops. uf p. Ztac.
  assert (He:inc v (powerset x)). app powerset_inc. rw H3. red. ir.
  nin H5. fold q in H6.  cp (intersection_forall H6 H5). unfold q in H5.
  Ztac. cp (powerset_sub H8). app H10.
  assert (Hf:inc w (powerset x)). app powerset_inc. rw H4. red. ir.
  cp (union_exists H6). nin H7.  nin H7. Ztac. cp (powerset_sub H9). app H11.
  assert (Hg:sub (W v f) v). red. ir. rw H3. app intersection_inc. ir.
  fold q in H7.  assert (sub v y). rw H3. app intersection_sub. ufi q H7. Ztac.
  cp (H2 _ _ He H9 H8). app H10.  app H11. 
  assert (Hh:sub w (W w f)). red. ir. rwi H4 H6. cp (union_exists H6). nin H7.
  nin H7. assert (sub x1 w). rw H4. app union_sub. Ztac.
  cp (H2 _ _ H10 Hf H9). app H12. app H11.
  split. apply extensionality. am. assert (inc v q). uf q. Ztac. cp (Hc _ H6).
  set (k:= W v f). rw H3. app intersection_sub.
  split. apply extensionality.  assert (inc w p). uf p. Ztac. cp (Hd _ H6).
  set (k:= W w f). rw H4. app union_sub. am. ir. split. app Ha. app Hb.
Qed.

Lemma exercise5_1: forall id x y,
  (forall i, inc i id -> sub (y i) (x i)) -> nonempty id ->
  productf id y = 
  intersectionf id (fun i=> inv_image_by_fun (pr_i (L id x) i) (y i)).
Proof. ir. set_extens. app intersectionf_inc. ir. uf inv_image_by_fun.
  assert (Ha: fgraph (L id x)). gprops.
  assert (Hb:is_function (pr_i (L id x) j)). app pri_function. bw.
  awi H1. ee. aw. exists (V j x0). split.  app H4. ue.
  assert (inc j (domain  (L id x))). bw.
  assert(inc x0 (productb (L id x))). aw. eee. bw.
  ir. rwi H3 H6. bw. app (H _ H6). app H4. ue.
  wr (pri_W Ha H5 H6). graph_tac. uf pr_i. rww bl_source.
  assert (inc (rep id) id). app nonempty_rep.
  cp (intersectionf_forall H1 H2). simpl in H3. ufi inv_image_by_fun H3.
  assert (Ha: fgraph (L id x)).  gprops.
  assert (Hb:is_function (pr_i (L id x) (rep id))). app pri_function. bw.
  awi H3. nin H3. nin  H3. red in H4. cp (inc_pr1graph_source Hb H4).
  ufi pr_i H5. awi H5. awii H5. nin H5; nin H6.
  aw. bwi H6.  split. am. split. am. ir.
  rwi H6 H8. cp (intersectionf_forall H1 H8). simpl in H9. 
  ufi inv_image_by_fun H9.
  assert (Hc:is_function (pr_i (L id x) i)). app pri_function. bw.
  awi H9. nin H9. nin  H9. red in H10. cp (W_pr Hc H10).
  rwi pri_W H11. ue. am. bw. aw. intuition. bw. am.
Qed.

Lemma exercise5_2: forall a b,
  bijective (BL(fun g => L a (fun x => image_by_graph g (singleton x)))
    (powerset (product a b)) (set_of_gfunctions a (powerset b))).
Proof. ir.
  set(tilde:=(BL (fun g => L a (fun x => image_by_graph g (singleton x)))
    (powerset (product a b)) (set_of_gfunctions a (powerset b)))).
  assert (transf_axioms
    (fun g => L a (fun x => image_by_graph g (singleton x)))
    (powerset (product a b)) (set_of_gfunctions a (powerset b))).
  red. ir. cp (powerset_sub H).
  set (faux:=BL(fun x=> image_by_graph c (singleton x)) a (powerset b)).
  assert(is_function faux).  uf faux. app bl_function. red. ir.
  ap powerset_inc. red. ir. awi H2. nin H2.  nin H2. cp (H0 _ H3).
  awi H4.  intuition. 
  cut (inc (graph faux) (set_of_gfunctions (source faux) (target faux))).
  uf faux. aw. uf BL.  aw. app inc_set_of_gfunctions.
  uf tilde. app bl_bijective. ir. 
  set (fx:= L a (fun x0 => image_by_graph u (singleton x0))).
  set (fy:= L a (fun x0 => image_by_graph v (singleton x0))).
  cp (powerset_sub H0).  cp (powerset_sub H1). 
  set_extens. cp (H3 _ H5). awi H6; ee.
  assert (inc (Q x) (V (P x) fy)). uf fy. wr H2. bw. aw.
  ex_tac. aw.  ufi fy H9. bwi H9. awi H9. nin H9. 
  nin H9. red in H10.  rwi (singleton_eq H9) H10. aw. awi H10. am. am. am.
  cp (H4 _ H5). awi H6. ee.  
  assert (inc (Q x) (V (P x) fx)). uf fx. rw H2. bw. aw.
  ex_tac. aw. ufi fx H9. bwi H9. awi H9. nin H9.
  nin H9. red in H10.  rwi (singleton_eq H9) H10. awi H10. am. am. am.
  ir. nin (set_of_gfunctions_inc H0). nin H1. ee.
  set (g:=Zo (product a b) (fun z => inc (Q z) (V (P z) y))).
  assert(inc g (powerset (product a b))).  app powerset_inc. red.  
  uf g. ir. Ztac. am.
  assert (Ha:is_graph g). red. uf g. ir. Ztac. awi H7. nin H7. am. 
  ex_tac. uf tilde. aw.  app fgraph_exten.
  gprops. wr H4. fprops. bw. wr H4. sy. aw. 
  ir.  assert (inc x0 a). bwi H6. am.  bw.
  sy. set_extens. change (inc x1 (im_singleton g x0)). rw im_singleton_pr. uf g. Ztac.
  app product_pair_inc. assert (sub (V x0 y) b). wr H4.
  change (sub (W x0 x) b).  wr powerset_inc_rw. wr H3. wri H2 H7. fprops.
  app H9. aw. awi H8. nin H8. nin H8. rwi (singleton_eq H8) H9. 
  ufi g H9. Ztac. awi H11. am. 
Qed.

Lemma exercise6_1: forall x g, is_graph g ->
  (is_equivalence g & substrate g = x) =
  (domain g = x & range g = x & 
    compose_graph g (compose_graph (inverse_graph g) g) = g
    & sub (identity_g x) g).
Proof. ir. app iff_eq. ir. nin H0. cp (domain_is_substrate H0).
  ir.  ee. ue. wr H1. uf substrate. set_extens. inter2tac. 
  nin (union2_or H3). aw.  exists x0.
  rwi H2 H4. equiv_tac. am.
  set_extens. awi H3. nin H3. nin H4. nin H4. awi H4. nin H4. nin H6. nin H6. 
  awi H7. assert (inc (J x2 x1) g). equiv_tac. assert (inc (J (P x0) x1) g).
  equiv_tac. assert (inc (J (P x0) (Q x0)) g).  equiv_tac.  awi H10. am. am.
  assert (is_pair x0). app H. assert (J (P x0) (Q x0) = x0). aw.
  assert (inc (J (P x0) (P x0)) g). equiv_tac. substr_tac.
  aw. split. am. exists (P x0). split. aw. split. fprops.
  ex_tac. aw. ue.
  red. ir. rwi inc_diagonal_rw H3.  ee.
  assert (J (P x0) (Q x0) = x0). aw. wr H6. wr H5. wri H1 H4. equiv_tac. 

  ir. assert (substrate g  = x). ee. uf substrate. rw H0. rw H1. ap union2idem.
  assert (forall u, inc u x -> inc (J u u) g). ir. ee. app H5.
  rw inc_diagonal_rw. split.  fprops. aw. au. 
  assert (is_symmetric g). red. split. am. ir. red in H3. ee.
  assert (inc (J y y) g). app H2. wr H4. aw. ex_tac.
  assert (inc (J x0 x0) g). app H2. wr H0. aw. ex_tac. 
  red. wr H5. aw. split. fprops. ex_tac. aw.
  split. fprops. ex_tac. aw.
  intuition. red. ee; tv;split;tv. ir. red. app H2. ue.
  ir. red. wr H5. aw. split. fprops. red in H8. ex_tac. aw.
  split. fprops. red in H6. ex_tac. aw. app H2. wr H0. aw.  ex_tac. 
Qed.
  
Lemma exercise6_2: forall g, is_graph g ->
  compose_graph g (compose_graph (inverse_graph g) g) = g ->
  (is_equivalence (compose_graph (inverse_graph g) g) &
    substrate (compose_graph (inverse_graph g) g) = domain g &
    is_equivalence (compose_graph g (inverse_graph g)) &
    substrate (compose_graph g (inverse_graph g)) = range g).
Proof. ir. 
  assert(Ha:is_graph (inverse_graph g)). app inverse_graph_is_graph.
  assert (Hb:is_graph (compose_graph (inverse_graph g) g)). 
  app composition_is_graph. 
  assert (Hc:is_graph (compose_graph g (inverse_graph g))).  
  app composition_is_graph. 
  assert (forall x y z t, related g x y -> related g z y -> related g z t ->
    related g x t). ir. red. wr H0. aw. split. fprops. exists z.
  split. aw. split. fprops. exists y. split. am. aw. am.
  assert (Hd:substrate (compose_graph (inverse_graph g) g) = domain g).
  set_extens. rwi inc_substrate_rw H2. nin H2. nin H2. awi H2. nin H2. nin H3.
  nin H3. ex_tac.
  nin H2. awi H2.  nin H2. nin H3. nin H3. awi H4. ex_tac. am.
  awi H2. nin H2. wri H0 H2.  awi H2. nin H2. nin H3. nin H3. 
  cp (inc_pr1_substrate H3). awi H5. am. am. 
  assert (He:substrate (compose_graph g (inverse_graph g)) = range g).
  set_extens. rwi inc_substrate_rw H2. nin H2. nin H2. awi H2. nin H2. nin H3.
  nin H3. awi H3.  ex_tac. 
  nin H2. awi H2.  nin H2. nin H3. nin H3. ex_tac. am.
  awi H2. nin H2. wri H0 H2.  awi H2. nin H2. nin H3. nin H3. awi H3. 
  nin H3. nin H5. nin H5.
  assert (inc (J x2 x) (compose_graph g (inverse_graph g))). aw. 
  split. fprops. exists x1. split;am. 
  cp (inc_pr2_substrate H7). awi H8. am. am. 

  set (h:=  inverse_graph g). 
  split. rw equivalence_pr.  split. wr composition_associative. uf h. ue.
  rw inverse_compose.  fold h. assert (g = inverse_graph h). uf h. 
  rww inverse_graph_involutive. ue. 
  split. am. split. rw equivalence_pr.  split. rw composition_associative. 
  rwi composition_associative H0. fold  h in H0. rww H0. 
  rw inverse_compose. fold h. assert (g = inverse_graph h). uf h.
  rww inverse_graph_involutive. wrr H2. am. 
Qed.

Definition intersection_with x a := 
  BL(fun w=> intersection2 w a) (powerset x)(powerset x).
Definition intersection_with_canon x a :=
  BL (fun b => Zo(powerset x)(fun c=> intersection2 c a = b))
  (powerset a)(quotient (equivalence_associated (intersection_with x a))).

Lemma exercise6_3: forall a x,
  sub a x -> bijective (intersection_with_canon x a).
Proof. ir. 
  assert(Ha: forall u, sub u a -> intersection2 u a = u).
  ir. app extensionality. app intersection2sub_first.  
  red. ir. app intersection2_inc. app H0.
  assert (Hb:transf_axioms (fun w0 => intersection2 w0 a)
    (powerset x) (powerset x)). red. ir. app powerset_inc. 
  apply sub_trans with c. app intersection2sub_first. app powerset_sub. 
  assert (is_function (intersection_with x a)). 
  uf intersection_with. app bl_function.
  set(r:= equivalence_associated (intersection_with x a)).
  assert (is_equivalence r). uf r. app graph_ea_equivalence.
  assert (transf_axioms (fun b => Zo(powerset x)
    (fun c=> intersection2 c a = b)) (powerset a)(quotient r)).
  red. ir. cp (powerset_sub H2). 
  set (w:= Zo (powerset x) (fun c0 => intersection2 c0 a = c)).
  assert(nonempty w). exists c. uf w. Ztac. app powerset_inc. 
  apply sub_trans with a. am. am. 
  assert (sub w (powerset x)). uf w. app Z_sub. 
  assert(inc (rep w) (powerset x)).  app H5. app nonempty_rep. 
  rw inc_quotient. red. split. am. split. uf r. rw graph_ea_substrate. 
  uf intersection_with. aw.  awi H6. am. am.
  assert(intersection2 (rep w) a = c).
  set (b:= rep w). assert (inc b w). uf b. app nonempty_rep. ufi w H7.
  Ztac. am.
  set_extens. bw. uf r. rw ea_related. uf intersection_with.
  assert (Hc :sub x0 x).  cp (H5 _ H8). awi H9. am. awi H6.
  aw. eee.  ufi w H8. Ztac. sy; am. am.
  bwi H8. ufi r H8. rwi ea_related H8.  ufi intersection_with H8. ee.
  awi H9. awii H10. uf w. Ztac. aw.  ue. aw. am.  am. am. 
  uf intersection_with_canon.
  red.  split. red. split. app bl_function. aw. ir.
  awi H5.  cp (powerset_sub H3). cp (powerset_sub H4).
  assert (inc x0 (Zo (powerset x) (fun c => intersection2 c a = y))).
  wr H5. Ztac. app powerset_inc. apply sub_trans with a. am. am. Ztac.
  sy. wr H10.  app Ha. am. am. am. am.
  app surjective_pr6. app bl_function. aw. 
  ir. rwi inc_quotient H3. nin H3. clear H3. nin H4.
  rwi graph_ea_substrate H3. simpl in H3. 
  assert(inc (intersection2 (rep y) a) (powerset a)). app powerset_inc.
  app intersection2sub_second. 
  cp (powerset_sub H5). ex_tac. aw. cp H3. ufi intersection_with H3. awi H3.
  set_extens. Ztac. rw H4. bw. rw ea_related. awi H9.  eee.
  uf intersection_with. aw.  uf intersection_with. sy; aw. am.
  rwi H4 H8.  bwi H8.  bwi H8. ufi intersection_with H8.
  rwi ea_related H8. ee. awi H9. awi H8. awi H10. Ztac. aw. am. aw. am. aw. am.
  am. am. am.
Qed.

Lemma exercise6_4: forall g a b x,
  let comp := compose_graph in let inter:= intersection2 in
  is_equivalence g -> is_graph a -> is_graph b -> substrate g = x -> sub a g ->
  (domain a = x -> comp g a = g &
  range a = x -> comp a g = g &
  (domain a = x -> comp (inter g b) a = inter g (comp b a)) &
  (range a = x -> comp a (inter g b)  = inter g (comp a b))).
Proof. ir. assert (Ha: is_graph g). fprops.
  split. ir. uf comp. set_extens. awi H5. nin H5. nin H6. nin H6.
  cp (H3 _ H6). assert (J (P x0) (Q x0) = x0). aw. wr H9. equiv_tac.
  cp (Ha _ H5). assert (J (P x0) (Q x0) = x0). aw.
  assert (inc (P x0) (domain a)). rw H4. wr H2. substr_tac. 
  awi H8. nin H8. aw. split. am. exists x1. split. am.
  cp (H3 _ H8). wri H7 H5. 
  assert (inc (J x1 (P x0)) g).  equiv_tac. equiv_tac. am.

  split. ir. uf comp. set_extens. awi H5. nin H5. nin H6. nin H6.
  cp (H3 _ H7). assert (inc (J (P x0) (Q x0)) g). equiv_tac. awi H9. am. am.
  assert (J (P x0) (Q x0) = x0). aw. app Ha.
  assert (inc (Q x0) (range a)). rw H4. wr H2.  substr_tac.
  awi H7. nin H7. aw. split. app Ha. exists x1. split. cp (H3 _ H7).
  wri H6 H5. assert (inc (J (Q x0) x1) g). equiv_tac. equiv_tac. am. am.

  split. ir. uf comp; uf inter. set_extens. awi H5. nin H5. nin H6. nin H6.
  nin (intersection2_both H7). assert (J (P x0) (Q x0) = x0). aw.
  wr H10. app intersection2_inc. cp (H3 _ H6). equiv_tac.
  aw. split. am. exists x1. intuition. 
  nin (intersection2_both H5).  assert (J (P x0) (Q x0) = x0). aw. app Ha.
  assert (inc (P x0) (domain a)). rw H4. wr H2. substr_tac. 
  wri H8 H6. awi H7. nin H7.  nin H10.  nin H10. aw. split. am. ex_tac.
  app intersection2_inc. cp (H3 _ H10). 
  assert (inc (J x1 (P x0)) g). equiv_tac.  equiv_tac.

  ir. uf comp. uf inter. set_extens. awi H5. nin H5. nin H6. nin H6.
  nin (intersection2_both H6).
  assert (J(P x0) (Q x0) = x0). aw. app intersection2_inc.
  wr H10. cp (H3 _ H7).  equiv_tac. aw.  split. am. ex_tac.  
  nin (intersection2_both H5). 
  assert (is_pair x0). app Ha. awi H7. nin H7. nin H9. nin H9.
  aw. split. am. exists x1. split. app intersection2_inc.
  cp (H3 _ H10). assert (inc (J (Q x0) x1) g). equiv_tac.
  assert (J(P x0) (Q x0) = x0). aw. wri H13 H6. equiv_tac. am.
Qed.

Lemma symmetric_union: forall a b, is_symmetric a -> is_symmetric b ->
  is_symmetric (union2 a b).
Proof. red. ir. red in H; nin H. red in H0; nin H0.
  split. red. ir. nin (union2_or H3). app H. app H0.
  ir. red in H3. nin (union2_or H3). red. app union2_first. 
  app H1. red. app union2_second. app H2.
Qed.

Lemma substrate_union_diag: forall x g,
  sub g (coarse x) -> substrate (union2 g (identity_g x)) = x.
Proof. ir. ufi coarse H. assert (is_graph g). red. ir. cp (H _ H0).
  awi H1. ee. am.
  assert(is_graph (union2 g (identity_g x))). red. ir. nin (union2_or H1).
  app H0. rwi inc_diagonal_rw H2. nin H2. am.
  set_extens.  rwi inc_substrate_rw H2. nin H2.
  nin H2. nin (union2_or H2). cp (H _ H3).  awi H4. eee.
  rwi inc_pair_diagonal H3. nin H3. am. nin H2.
  nin (union2_or H2). cp (H _ H3).  awi H4. eee.
  rwi inc_pair_diagonal H3. nin H3.  ue. am.
  assert (inc (J x0 x0) (union2 g (identity_g x))). app union2_second.
  rw inc_pair_diagonal. au.  assert (x0 = P (J x0 x0)). aw. rw H4. substr_tac. 
Qed.

Definition special_equivalence a b x :=
  union2 (doubleton (J a b) (J b a))(identity_g x).
Lemma substrate_special_equivalence:forall a b x,
  inc a x -> inc b x ->  substrate(special_equivalence a b x) = x.
Proof. ir. uf special_equivalence. app substrate_union_diag. red. ir.
  uf coarse. nin (doubleton_or H1); rw H2; fprops. 
Qed.

Lemma special_equivalence_ea:forall a b x,
  inc a x -> inc b x -> is_equivalence(special_equivalence a b x).
Proof. ir.
  assert (is_graph (special_equivalence a b x)). uf special_equivalence.
  red. ir. nin (union2_or H1). nin (doubleton_or H2); rw H3; fprops.
  rwi inc_diagonal_rw H2. nin H2. am.
  app symmetric_transitive_equivalence. 
  red. split. am. uf special_equivalence. ir. red in H2. nin (union2_or H2).
  red.  app union2_first.
  nin (doubleton_or H3); [cut (J y x0 = J b a) | cut (J y x0 = J a b)]; ir;
  try (rw H5; fprops);  rw (pr1_def H4); rw (pr2_def H4); tv.
  red. app union2_second.
  rwi inc_pair_diagonal H3. rw inc_pair_diagonal. intuition. ue.
  red. split. ir. am. uf related. uf special_equivalence. ir.
  nin (union2_or H2).  nin (doubleton_or H4). rw (pr1_def H5). 
  nin (union2_or H3).  nin (doubleton_or H6). rw (pr2_def H7). 
  app union2_first. fprops. rw (pr2_def H7). 
  app union2_second. rw inc_pair_diagonal. au.
  rwi inc_pair_diagonal H6. nin H6. wr H7. rwi (pr1_def H5) H2. am.
  rw (pr1_def H5). nin (union2_or H3). nin (doubleton_or H6).
  rw (pr2_def H7). app union2_second. rww inc_pair_diagonal. au.
  rw (pr2_def H7). app union2_first. fprops.
  rwi inc_pair_diagonal H6. nin H6. wr H7.
  rw (pr2_def H5).  app union2_first.  fprops.
  rwi inc_pair_diagonal H4. nin H4. rww H5.
Qed.

Lemma exercise6_5: let x := three_points in 
  let g1:= special_equivalence (Ro tpa) (Ro tpb) x in
    let g2:= special_equivalence (Ro tpa) (Ro tpc) x in
      (is_equivalence g1 & is_equivalence g2 & substrate g1 = x &  
        substrate g2 = x &  ~ (is_equivalence (union2 g1 g2))).
Proof. ir. 
  split. uf g1. app special_equivalence_ea. uf x. ap R_inc. uf x; ap R_inc. 
  split. uf g2. app special_equivalence_ea. uf x. ap R_inc. uf x; ap R_inc. 
  split. uf g1; uf x. rww substrate_special_equivalence. ap R_inc. ap R_inc. 
  split. uf g2; uf x. rww substrate_special_equivalence. ap R_inc. ap R_inc.
  red. ir. 
  assert (related (union2 g1 g2) (Ro tpb) (Ro tpa)). red. app union2_first.
  uf g1. uf special_equivalence. app union2_first. fprops.
  assert (related (union2 g1 g2) (Ro tpa) (Ro tpc)). red. app union2_second.
  uf g2. uf special_equivalence. app union2_first. fprops.
  assert (related (union2 g1 g2) (Ro tpb) (Ro tpc)). equiv_tac.

  red in H2. nin (union2_or H2). nin (union2_or H3).
  nin (doubleton_or H4). cp (pr1_def H5).  disc. 
  cp (pr2_def H5). disc.  rwi inc_diagonal_rw H4. nin H4. nin H5. 
  awi H6. disc.
  nin (union2_or H3). nin (doubleton_or H4). cp (pr1_def H5).  
  disc. cp (pr2_def H5). disc.  
  rwi inc_diagonal_rw H4. nin H4. nin H5. awi H6. disc.
Qed.
     
Lemma exercise6_6a: forall G H,
  is_equivalence G -> is_equivalence H ->
  (is_equivalence (compose_graph G H) = 
    (compose_graph G H = compose_graph H G)).
Proof. ir. set (K:= compose_graph G H).
  app iff_eq. ir.
  set_extens. assert (is_pair x). ufi K H3. awi H3. eee.
  assert (J (P x)(Q x) = x). aw. wri H5 H3. 
  assert (inc (J (Q x) (P x)) K). equiv_tac. ufi K H6. awi H6. nin H6. nin H7.
  nin H7. aw. split. am. exists x0. split; equiv_tac. 
  awi H3. nin H3. nin H4. nin H4.  assert (J (P x)(Q x) = x). aw.
  wr H6. cut (inc (J (Q x) (P x)) K). ir. equiv_tac. uf K. aw. split. 
  fprops. exists x0.  split; equiv_tac. 

  ir.  rwi equivalence_pr H1. rwi equivalence_pr H0.
  rw equivalence_pr. ee. uf K. rw composition_associative.
  ufi K H2. rw H2. wr (composition_associative G G H). rw H0.
  wr composition_associative. rw H2. rw composition_associative. rww H1.
  uf K. rw inverse_compose. wr H4; wr H3. am.
Qed.

Lemma exercise6_6b: forall G H,
  is_equivalence G -> is_equivalence H ->  substrate G = substrate H -> 
  substrate (compose_graph G H) = substrate G.
Proof. ir. 
  set_extens. ufi substrate H3. nin (union2_or H3); awi H4;
  nin H4; awi H4; nin H4; fprops; nin H5; nin H5. 
  assert (x = P (J x x1)). aw. rw H7. rw H2. substr_tac.
  assert (x = Q (J x1 x)). aw. rw H7. substr_tac.
  assert (related G x x). equiv_tac.  
  assert (related H x x). rwi H2 H3. equiv_tac.  
  assert (related  (compose_graph G H) x x). red. aw. split. fprops. 
  exists x. au. substr_tac.
Qed.

Lemma exercise6_6c: forall G H,
  is_equivalence G -> is_equivalence H -> substrate G = substrate H ->
  (sub G (compose_graph G H) & sub H (compose_graph G H)
    &forall W, is_equivalence W -> sub G W -> sub H W ->
      sub (compose_graph G H) W).
Proof. ir. assert (is_graph G). fprops.
  assert (is_graph H). fprops.
  assert (is_graph  (compose_graph G H)). ap composition_is_graph.
  split. red. ir. cp (H3 _ H6). assert (J (P x)(Q x) =x). aw. 
  wr H8. aw. split. wr H8. fprops. wri H8 H6.  ex_tac.
  assert (inc (P x) (substrate H)). wr H2. rwi H8 H6; substr_tac. equiv_tac.  
  split. red. ir.  cp (H4 _ H6). assert (J (P x)(Q x) =x). aw.
  wr H8. aw. split. wr H8. fprops. wri H8 H6; ex_tac.
  assert (inc (Q x) (substrate G)). rw H2. rwi H8 H6. substr_tac. equiv_tac. 
  ir. red. ir. assert (is_pair x). app H5. assert (J (P x)(Q x) =x). aw. 
  wri H11 H9. awi H9. nin H9. nin H12. nin H12.
  cp (H8 _ H12).  cp (H7 _ H13). wr H11. equiv_tac. am.
Qed.
    
Lemma range_is_substrate: forall g,
  is_equivalence g -> range g = substrate g.
Proof. ir. uf substrate. set_extens. inter2tac. 
  nin (union2_or H0). awi H1. nin  H1. aw. exists x0. 
  equiv_tac.  fprops. fprops. am.
Qed.

Lemma sub_coarse: forall g,
  is_equivalence g ->  sub g (coarse (substrate g)).
Proof. ir. assert (is_graph g). fprops. cp (sub_graph_prod H0).
  rwi range_is_substrate H1. rwi domain_is_substrate H1. am. am. am.
Qed.

Lemma exercise6_6d: forall G H,
  is_equivalence G -> is_equivalence H -> substrate G = substrate H ->
  compose_graph G H = compose_graph H G ->
  (compose_graph G H) = intersection(Zo (powerset (coarse (substrate G)))
    (fun W =>  is_equivalence W & sub G W & sub H W)).
Proof. ir. set (E:= substrate G). assert (sub G (coarse E)). uf E.
  app sub_coarse. assert (sub H (coarse E)). uf E. rw H2. app sub_coarse.
  cp (exercise6_6c H0 H1 H2).
  set_extens. app intersection_inc. exists (coarse E).
  Ztac. ap powerset_inc. fprops. split. ap coarse_equivalence. au.
  ir. Ztac. ee. cp (H14 _ H10 H11 H12). app H15. 
  wri (exercise6_6a H0 H1) H3.  
  ap (intersection_forall  (y:=(compose_graph G H)) H7).
  Ztac. app powerset_inc. uf E. wr (exercise6_6b H0 H1 H2). app sub_coarse.
  split. am. intuition. 
Qed.

Remark exercise6_7: forall G0 G1 H0 H1 E x,
  is_equivalence G0 -> substrate G0 = E ->
  is_equivalence H0 -> substrate H0 = E ->
  is_equivalence G1 -> substrate G1 = E ->
  is_equivalence H1 -> substrate H1 = E ->
  intersection2 G1 H0 = intersection2 G0 H1 ->
  compose_graph G1 H0 = compose_graph G0 H1 ->
  inc x E -> (
    let G1x := image_by_graph G1 (singleton x) in 
      let H1x := image_by_graph H1 (singleton x) in
        let R0 := induced_relation G0 G1x in
          let S0 := induced_relation H0 H1x in
            equipotent (quotient R0) (quotient S0)).
Proof. ir. set (A:= intersection2 G1x H1x).
  set(Ar :=induced_relation R0 A).
  set(As :=induced_relation S0 A).
  assert (Ha: is_graph G0). fprops.
  assert (Hb: is_graph H0). fprops.
  assert (Hc: is_graph G1). fprops.
  assert (Hd: is_graph H1). fprops.
  assert (He:induced_rel_axioms G0 G1x). red. split. am. rw H2. uf G1x. red. ir.
  awi H12. nin H12. nin H12. red in H13. wr H6. app (inc_arg2_substrate H13). 
  assert (Hf:induced_rel_axioms H0 H1x). red. split. am. rw H4. uf H1x. red. ir.
  awi H12. nin H12. nin H12. red in H13. wr H8. app (inc_arg2_substrate H13).
  assert (is_equivalence R0). uf R0. app induced_rel_equivalence.
  assert (is_equivalence S0). uf S0. app induced_rel_equivalence.
  assert (forall u, inc u G1x = related G1 x u). ir. uf G1x.  aw.
  app iff_eq. ir. nin H14. nin H14. rwi (singleton_eq H14) H15. am.
  ir.  ex_tac.
  assert (forall u, inc u H1x = related H1 x u).  ir. uf H1x.  aw.
  app iff_eq. ir. nin H15. nin H15. rwi (singleton_eq H15) H16. am.
  ir.  ex_tac.
  assert(forall u v, related R0 u v = 
    (related G1 x u & related G1 x v & related G0 u v)).
  ir.  uf R0. rw (induced_rel_related u v He). rw H14; rw H14. tv.
  assert(forall u v, related S0 u v = 
    (related H1 x u & related H1 x v & related H0 u v)).
  ir.  uf S0. rw (induced_rel_related u v Hf). rw H15; rw H15. tv.
  assert(induced_rel_axioms R0 A). red.  split. am. red. ir.
  ufi A H18. assert (related R0 x0 x0). rw H16. cp (intersection2_first H18).
  ufi G1x H19. awi H19. nin H19. nin H19. rwi (singleton_eq H19) H20.
  split. am. split. am. app reflexivity_e. rw H2. wr H6. substr_tac.
  substr_tac.
  assert(induced_rel_axioms S0 A). red.  split. am. red. ir.
  ufi A H19. assert (related S0 x0 x0). rw H17. cp (intersection2_second H19).
  ufi H1x H20. awi H20. nin H20. nin H20. rwi (singleton_eq H20) H21.
  split. am. split. am. app reflexivity_e. rw H4. wr H8. 
  substr_tac.  substr_tac.
  assert (is_equivalence  Ar). uf Ar. app induced_rel_equivalence.
  assert (is_equivalence  As). uf As. app induced_rel_equivalence.
  assert (forall u, inc u A = (related G1 x u & related H1 x u)). 
  ir. uf A. uf G1x. uf H1x. app iff_eq. ir. nin (intersection2_both H22).
  split. awi H23. nin H23. nin H23. rwi (singleton_eq H23) H25. am.
  awi H24. nin H24. nin H24. rwi (singleton_eq H24) H25. am.
  ir. nin H22. app intersection2_inc; aw; ex_tac. 
  assert(forall u v, related Ar u v = (related G1 x u & related G1 x v &
    related H1 x u & related H1 x v  & related G0 u v)). 
  ir. uf Ar. rw (induced_rel_related u v H18). rw H16. rw H22. rw H22.
  app iff_eq. intuition. intuition.
  assert(forall u v, related As u v = (related G1 x u & related G1 x v &
    related H1 x u & related H1 x v  & related H0 u v)).
  ir. uf As. rw (induced_rel_related u v H19). rw H17. rw H22. rw H22.
  app iff_eq. intuition. intuition.
  assert (forall u v, related Ar u v = related As u v).
  ir. rw H23; rw H24. ap iff_eq. ir. eee.
  assert (related H1 u v). apply transitivity_e with x. am.
  app symmetricity_e. am. assert (inc (J u v) (intersection2 G0 H1)).
  app intersection2_inc. red. wri H9 H31. app (intersection2_second H31).
  ir. eee.  assert (related G1 u v). apply transitivity_e with x. am.
  app symmetricity_e. am. assert (inc (J u v) (intersection2 G0 H1)). wr H9.
  app intersection2_inc. red. app (intersection2_first H31).
  assert (equipotent (quotient Ar) (quotient As)).
  assert (Ar = As). rw graph_exten. am. fprops.  fprops. 
  rw H26. ap equipotent_reflexive.
Abort.

Lemma exercise6_8: forall f r,
  is_equivalence r -> is_function f -> target f = substrate r ->
  (exists g, bijective g & source g = quotient (inv_image_relation f r) & 
    target g = quotient (induced_relation r (image_of_fun f))).
Proof. ir.  set (s := inv_image_relation f r). 
  set (A:= (image_of_fun f)). set (Ra := induced_relation r A).
  assert (iirel_axioms f r). red. intuition. assert (A = range (graph f)).
  uf A. uf image_of_fun. red in H0. nin H0. nin H3. rw  H4.
  rw image_by_graph_domain. tv. fprops.
  assert (is_equivalence s).  uf s. app iirel_relation.
  assert (induced_rel_axioms r A). red. split. am. wr H1. rw H3. 
  app corresp_sub_range. red in H0; nin H0; am.
  assert (is_equivalence Ra). uf Ra.  app induced_rel_equivalence.
  set (f1:= fun x=>  fun y => is_class r y 
    & nonempty (intersection2 y A) & x = inv_image_by_fun f y).
  assert(forall x, inc x (quotient s) -> exists y, f1 x y). ir.
  rwi inc_quotient H7. ufi s H7. rwi (iirel_class x H2) H7. nin H7. 
  exists x0. uf f1. rw H3. am. am.
  set (f2:= fun x => choose (fun y => f1 x y)).
  assert (forall  x, inc x (quotient s) -> f1 x (f2 x)). 
  ir. uf f2. app choose_pr.  app (H7 _ H8). 
  set (f3:= fun x => intersection2 (f2 x) A).
  assert (forall x,  inc x (quotient s) -> inc (f3 x) (quotient Ra)).
  ir. uf Ra. cp (H8 _ H9). ufi f1 H10. rw inc_quotient. rw induced_rel_class.
  exists (f2 x). intuition. am. am.
  set (g:= BL f3 (quotient s) (quotient Ra)).
  exists g. eee. uf g; app bl_bijective.
  ir. ufi f3 H12. cp (H8 _ H10). cp (H8 _ H11).  ufi f1 H13. ufi f1 H14. ee.
  nin H15. assert (inc y (f2 v)). inter2tac.
  assert (inc y (f2 u)). wri H12 H15. inter2tac.
  assert (inc y (range (graph f))). wr H3. inter2tac.
  awi H21. nin H21. assert (inc x u). rw H18. uf inv_image_by_fun. aw. 
  ex_tac. assert (inc x v). rw H16.
  uf inv_image_by_fun. aw.  ex_tac.
  rwi inc_quotient H10. rwi inc_quotient H11. nin (class_dichot H10 H11).
  am. elim (emptyset_pr (x:=x)).  wr H24. app intersection2_inc. am. am. fprops.
  ir. rwi inc_quotient H10. ufi Ra H10.
  rwi induced_rel_class H10. nin H10. nin H10.
  set (u:= inv_image_by_fun f x).
  assert (inc u (quotient s)). uf s. rw inc_quotient. rw iirel_class. 
  exists x. wr H3. intuition. am. am.  ex_tac.
  uf f3. cp (H8 _ H12). ufi f1 H13.
  nin H11. nin H11. nin (intersection2_both H11). rwi H3 H16. awi H16. 
  nin H16. assert (inc x0 u). uf u. uf inv_image_by_fun. aw. ex_tac.
  nin H13. nin H18.
  rwi H19 H17.  ufi inv_image_by_fun H17. awi H17. nin H17. nin H17.
  assert (x1 = y0). wr (W_pr H0 H16).  wr (W_pr H0 H20). tv.
  nin (class_dichot H10 H13). sy. ue.
  elim (emptyset_pr (x:=y0)). wr H22.  app intersection2_inc. ue.
  fprops. am. am.  uf g. aw. uf g. aw.
Qed.

Lemma exercise6_9: forall F G p f r,
  is_equivalence r ->  F = substrate r -> p = canon_proj r ->
  surjective f -> source f = G -> target f = quotient r ->
  exists E, exists g, exists h,
  (surjective g & surjective h & source g = E & source h = E &  target g = F 
    & target h = G & compose p g = compose f h).
Proof. ir. set (a:= TPa). set (b:= TPb).
  assert (Hab: b <> a). uf a; uf b. app two_points_distinctb.
  set (Ea:= product F (singleton a)). set (Eb:=product G (singleton b)).
  set (E:= union2 Ea Eb).
  assert (Ha:is_graph E). uf E; uf Ea; uf Eb. red. ir. 
  nin (union2_or H5);  awi H6; nin H6; am.  
  assert (Hb:forall x, inc x E -> (Q x =a \/ Q x = b)). 
  uf E; uf Ea; uf Eb. ir. nin (union2_or H5); awi H6; ee; au.  
  assert (Hc:forall x, inc x G -> inc (W x f) (quotient r)).
  ir. wr H4. app inc_W_target. fct_tac. ue.
  assert (Hd:forall x, inc x G -> inc (rep (W x f)) F). ir. rw H0. fprops.
  set (gz :=fun z=> Yo (Q z = a) (P z) (rep (W (P z) f))).
  assert (He:forall z, inc z Ea -> gz z = P z). uf Ea.
  ir. awi H5. ee. uf gz. rww Y_if_rw. 
  assert (Hf:forall z, inc z Ea -> inc (gz z) F).
  ir. rw He. ufi Ea H5. awi H5. intuition. am.
  assert (Hg:forall z, inc z Eb -> gz z = rep (W (P z) f)). uf Eb. ir.
  awi H5. ee. uf gz. rww Y_if_not_rw.  ue.
  assert (Hh:forall z, inc z Eb -> inc (gz z) F). ir. rw Hg. ap Hd.
  ufi Eb H5. awi H5. intuition. am.
  assert (transf_axioms gz E F). red.  ir. ufi E H5. nin (union2_or H5).
  app Hf. app Hh.
  set (g:= BL gz E F). 
  assert(surjective g). uf g. app bl_surjective. ir.
  assert (inc  (J y a) Ea). uf Ea. fprops. 
  assert (inc  (J y a) E). uf E. inter2tac.
  ex_tac. rw He.  aw. am.
  assert(forall x, inc x Eb -> W (W x g) (canon_proj r) = W (P x) f).
  ir. uf g. aw. rw Hg. app class_rep. app Hc.
  ufi Eb H7. awi H7. nin H7. nin H8. am. am. uf E. inter2tac.
  wr H0. app Hh. uf E.  inter2tac.
  set (ha:= fun x => (rep (inv_image_by_fun f(singleton(W x (canon_proj r)))))).
  assert (Hi:forall x, inc x F -> 
    ha x = rep (inv_image_by_fun f (singleton (class r x)))).
  ir. uf ha. aw. ue.
  assert (Hj:forall x, inc x F -> 
    sub (inv_image_by_fun f (singleton(class r x))) G).
  ir. red. ir. ufi inv_image_by_fun H9. awi H9. nin H9. nin H9.
  red in H2; nin H2.  wr H3. graph_tac.
  assert(Hk:forall x, inc x F -> 
    inc (ha x) (inv_image_by_fun f (singleton (class r x)))).
  ir. rw Hi. app nonempty_rep.
  assert (inc (class r x) (target f)). rw H4. rwi H0 H8. gprops.
  nin (surjective_pr2 H2 H9). nin H10. exists x0.
  uf inv_image_by_fun. aw. exists (class r x). split. fprops. red. wr H11.
  ap W_pr3. fct_tac. am. am. 
  assert (Hl:forall x, inc x F -> inc (ha x) G). ir. ap (Hj _ H8). app Hk. 
  set(hz:= fun z=> Yo (Q z = a) (ha (P z)) (P z)).
  assert (forall z, inc z E -> inc (hz z) G). uf E; uf Ea; uf Eb.
  ir. nin(union2_or H8); awi H9; uf hz; ee; rw H11.
  rww Y_if_rw. app Hl. rww Y_if_not_rw. 
  set(h:=BL hz E G).
  assert(surjective h). uf h. app bl_surjective. ir.
  assert (inc (J y b) Eb). uf Eb. fprops.
  assert (inc (J y b) E). uf E. inter2tac.
  ex_tac. uf h. aw. uf hz.  rw Y_if_not_rw. aw. aw. 
  assert(forall x, inc x Ea -> W (W x h) f = W (P x) (canon_proj r)).
  ir. uf h. aw. uf hz.  ufi Ea H10. awi H10. ee.
  rw Y_if_rw. cp (Hk _ H11). ufi inv_image_by_fun H13. awi H13. nin H13.
  nin H13. red in H14. red in H2. nin H2. rw (W_pr H2 H14). 
  db_tac. am.  uf E. inter2tac.
  wr H0. ufi Ea H10. awi H10. ee. am.

  exists E. exists g. exists h. eee. uf g. aw. uf h. aw. uf g. aw. uf h. aw.
  assert (composable p g). red. split. rw H1. app canon_proj_function. split.
  fct_tac. rww H1.  sy. uf g. aw. 
  assert (composable f h). red. split. fct_tac.  split. fct_tac.  uf h. aw.
  assert (Hm: source g = source h). uf g; uf h; aw.
  ap function_exten. assert (is_function g). fct_tac. fct_tac.  
  assert (is_function f). fct_tac. fct_tac. aw. sy;  rww H1.  aw.
  ir. awi H13. aw. ufi g H13. awi H13. 
  ufi E H13. nin (union2_or H13). rw H10. uf g. aw. rw He. rw H1. aw. 
  wr He. wr H0. app Hf. am. am. wr He. wr H0. app Hf. am. am. 
  uf h. uf hz.  aw. rw Y_if_not_rw. rw H1. app H7. ufi Eb H14. awi H14. ee. 
  rww H16. ue.
Qed.

Section Exercice6_10.
Lemma Exercise6_10_a: forall r:EEP,
  symmetric_r (fun  x y => r x y & r y x).
Proof. ir. red. ir. intuition.
Qed.

Lemma exercise6_10_b: forall r E,
  reflexive_r r E -> reflexive_r (fun  x y => r x y & r y x) E.
Proof. uf reflexive_r. ir. rw H. app iff_eq. intuition. intuition. Qed.

Variables (R:EEP) (E:Set). 
Variables (A1: reflexive_r R E)(A2: symmetric_r R)
  (A3: forall x y, R x y -> inc x E).

Inductive chain:Type :=
  chain_pair: Set -> Set -> chain
 | chain_next: Set -> chain -> chain. 

Fixpoint chain_head x :=
  match x with chain_pair u _ => u | chain_next u _ => u end.
 
Fixpoint chain_tail x :=
  match x with chain_pair _ u => u | chain_next _ u => chain_tail u end.

Fixpoint chained_r x :=
  match x with chain_pair u v => R u v 
    | chain_next u v => R u (chain_head v) & chained_r v
 end.

Definition relS x y := exists c:chain, 
  chained_r c & chain_head c = x  & chain_tail c = y.

Fixpoint concat_chain x y {struct x} : chain :=
  match x with chain_pair u _ => chain_next u y 
| chain_next u v => chain_next u  (concat_chain  (x:=v) y) end.

Lemma head_concat : forall x y, 
  chain_head (concat_chain x y) = chain_head x.
Proof. ir. induction x; tv.  Qed.

Lemma tail_concat : forall x y, 
  chain_tail (concat_chain x y) = chain_tail y.
Proof. ir. induction x; tv. Qed.

Lemma chained_concat: forall x y, 
  chained_r x -> chained_r y -> chain_tail x = chain_head y ->
  chained_r (concat_chain x y).
Proof. ir. induction x. split. wrr H1. am.
  nin H. split. rww head_concat. app IHx.
Qed.

Lemma transitiveS: forall x y z, relS x y -> relS y z -> relS x z.
Proof. ir. nin H. nin H0. ee. exists (concat_chain x0 x1). split.
  app chained_concat.  ue. split. rww head_concat. rww tail_concat.
Qed.

Fixpoint reconc_chain (x y:chain) {struct x} :chain:=
  match x with chain_pair u v => chain_next v (chain_next u y)
   | chain_next u v => reconc_chain v (chain_next u y) end.

Lemma tail_reconc: forall x y, chain_tail (reconc_chain x y) = chain_tail y.
Proof. intro x.  induction x; ir; tv. simpl. rww IHx.
Qed.
Lemma head_reconc: forall x y, chain_head (reconc_chain x y) = chain_tail x.
Proof. intro x. induction x.  tv. ir. simpl. app IHx.
Qed.

Lemma chained_reconc: forall x y, chained_r x -> chained_r y -> 
  R (chain_head y) (chain_head x) ->  chained_r (reconc_chain x y).
Proof.  intro x. induction x; simpl; ir. au. ee;  app IHx. simpl. au.
Qed.

Fixpoint chain_reverse x:=
  match x with chain_pair u v => chain_pair v u
    | chain_next u v =>
      match v with chain_pair u' v' => chain_next v' (chain_pair u' u)
        | chain_next u' v' => reconc_chain v' (chain_pair u' u)
      end end.
Lemma head_reverse: forall x, chain_head (chain_reverse x) = chain_tail x.
Proof. ir. induction x. tv.  induction x. tv. simpl. app head_reconc.
Qed.
Lemma tail_reverse: forall x, chain_tail (chain_reverse x) = chain_head x.
Proof. ir. induction x. tv. induction x. tv. simpl. rww tail_reconc.
Qed.
Lemma chained_reverse: forall x, chained_r x -> chained_r (chain_reverse x).
Proof. ir. induction x. simpl. au. induction x; simpl; simpl in H; ee. 
  au. au.  app chained_reconc. simpl. au. 
Qed.

Lemma symmetricS:  forall x y, relS x y -> relS y x.
Proof. ir. red in H. nin H. ee. exists (chain_reverse x0). split.
  app chained_reverse. split. rww head_reverse. rww tail_reverse.
Qed.

Lemma equivalenceS: equivalence_re relS E.
Proof.  ir. red. split. red. split. red. ir. app symmetricS. red. ir.
  apply transitiveS with y. am. am. red. ir. app iff_eq. ir.
  exists (chain_pair y y). split.  simpl. wrr A1. simpl. intuition.
  ir. red in H. nin H. ee. nin x. simpl in H. simpl in H0. wr H0. app (A3 H).
  simpl in H. simpl in H0. wr H0. nin H. app (A3 H).
Qed.

Definition Sgraph := graph_on relS E.
Lemma equivalence_Sgraph: is_equivalence Sgraph.
Proof. uf Sgraph. cp (equivalence_has_graph0 equivalenceS).
  assert (is_graph (graph_on relS E)). app graph_on_graph.
  cp equivalenceS. nin H1.
  app (equivalence_if_has_graph2 H0 H H1).
Qed.
Lemma substrate_Sgraph: substrate Sgraph =E.
Proof. uf Sgraph. app extensionality. app graph_on_substrate. red. ir.
  assert (relS x x).  cp equivalenceS. nin H0. wr H1. am.
  cp equivalenceS. wri (graph_on_rw2 x x H1) H0. substr_tac.
Qed.

Lemma S_is_smallest: forall r, is_equivalence r -> 
  (forall x y, R x y -> inc (J x y) r) -> sub Sgraph r.
Proof. ir.
  assert (forall w, chained_r w -> inc (J (chain_head w) (chain_tail w)) r).
  ir. induction w. app H0. nin H1.  pose (H0 _ _ H1). pose (IHw H2).
  equiv_tac.
  red. uf Sgraph. uf graph_on. ir. Ztac. nin H4. nin H4. nin H5.
  assert (J (P x)(Q x) = x).  aw.  awi  H3; eee.
  wr H7. wr  H5. wr H6. app H1.
Qed.

Definition setF:= Zo (powerset E)(fun A => forall y z, inc y A ->
  inc z (complement E A) -> not (R y z)).
Definition connected_comp x := intersection(Zo setF (fun A => inc x A)). 

Lemma setF_pr: forall A a b,
  inc A setF -> inc a A -> R a b -> inc b A.
Proof. ir. ufi setF H. Ztac. nin (inc_or_not b A). tv. ir.
  assert (inc b (complement E A)). srw. split.
  assert (R b a). app A2. app (A3 H5). am. pose (H3 _ _ H0 H5). contradiction.
Qed. 

Lemma setF_pr2: forall A a b,
  inc A setF -> inc a A -> relS a b -> inc b A.
Proof. ir. red in H1. nin H1. ee. wr H3. wri H2 H0. clear H2; clear H3.
  induction x; simpl in *. ap (setF_pr H H0 H1). 
  nin H1. cp (setF_pr H H0 H1). app IHx.
Qed.
Lemma setF_pr3: forall A a, inc A setF -> inc a A -> sub (class Sgraph a) A.
Proof. ir. red. ir. bwi H1. ufi Sgraph H1. rwi graph_on_rw2 H1.
  ap (setF_pr2 H H0 H1). ap equivalenceS. ap equivalence_Sgraph. 
Qed.
Lemma setF_pr4: forall a, inc a E -> inc (class Sgraph a) setF.
Proof. ir. uf setF. cp equivalence_Sgraph. Ztac. ap powerset_inc. 
  wr substrate_Sgraph. app sub_class_substrate. 
  ir. srwi H2. nin H2. red. ir. app H3. bwi H1. bw. 
  assert (related Sgraph y a). equiv_tac.  cp equivalenceS.
  ufi Sgraph H5. rwi graph_on_rw2 H5. nin H5. ee. 
  assert (related Sgraph z a).
  uf Sgraph. rw graph_on_rw2. red.
  exists (chain_next z x). split. simpl. rw H7. au. simpl. au. am. 
  equiv_tac. am. am.
Qed.

Lemma connected_comp_class: forall x, inc x E ->
  class Sgraph x = connected_comp x.
Proof. ir. set_extens. uf connected_comp. app intersection_inc. exists E. Ztac. 
  uf setF. Ztac. app powerset_inc. fprops. ir. srwi H2.
  nin H2. elim H3. am. ir. Ztac. ap (setF_pr3 H2 H3). am.
  ufi connected_comp H0. 
  cp equivalence_Sgraph.
  assert (inc  (class Sgraph x)  (Zo setF (fun A => inc x A))). Ztac.
  app setF_pr4.  wri substrate_Sgraph H. bw. equiv_tac.
  ap (intersection_forall H0 H2).
Qed.

Definition intransitive1 := forall x y z t,
  x <> y ->  R x y -> R x z -> R x t -> R y z -> R y t -> R z t.

Lemma intransitive1pr : 
  let intransitive_alt:= forall x y z t,
    x <> y -> x <> z -> x <> t -> y <> z -> y <> t -> z <> t ->
    inc x E -> inc y E -> inc z E -> inc t E -> 
    R x y -> R x z -> R x t -> R y z -> R y t -> R z t in
    intransitive1 = intransitive_alt.
Proof. uf intransitive1. app iff_eq. ir. app (H x y z t H0 H10 H11 H12 H13 H14).
  ir. nin (equal_or_not x z). ue.
  nin (equal_or_not x t). ue. app A2. 
  nin (equal_or_not y z). ue.
  nin (equal_or_not y t). ue. app A2.
  assert (inc z E). cp (A2  H4). app (A3 H10).
  nin (equal_or_not z t). ue. wrr A1.  ue.
  app (H x y z t). app (A3 H1). app (A3 H4). cp (A2 H5). app (A3 H12).
Qed.

Definition stableR A:= forall a b, inc a A -> inc b A -> R a b.
Definition Cab a b:= Zo E (fun x => R a x & R b x).

Lemma Cab_stable: forall a b, a<> b -> R a b -> intransitive1 ->
  stableR (Cab a b).
Proof. ir. red. ir. ufi Cab H2. Ztac. clear H2. ufi Cab H3. Ztac. ee. red in H1.
  app (H1 a b a0 b0).
Qed.
Lemma Cab_trans: forall a b x y, a<> b -> R a b -> intransitive1 ->
  x<> y -> inc x (Cab a b) -> inc y (Cab a b) -> (Cab a b)= (Cab x y).
Proof. ir. red in H1. ufi Cab H3. Ztac. ee. clear H3.
  ufi Cab H4. Ztac. clear H4.
  set_extens. ufi Cab H4. Ztac. ee. clear H4. uf Cab. Ztac. split. 
  app (H1 a b x x0). app (H1 a b y x0).
  ufi Cab H4. Ztac. clear H4. uf Cab. Ztac. ee.
  app (H1 x y a x0). app (H1 a b x y). app A2. app A2.
  app (H1 x y b x0). app (H1 a b x y). app A2. app A2.
Qed.

Lemma singleton_component: forall A, sub A E ->
  (inc A (quotient Sgraph) & is_singleton A) =
  (exists a, A = singleton a & forall b, R a b -> a = b).
Proof. ir. cp equivalence_Sgraph.  rename H0 into Ha.
  ap iff_eq. ir. ee. nin H1. exists x. split. am. ir.
  assert (related Sgraph x b). uf Sgraph. rw graph_on_rw2. red.
  exists (chain_pair x b). simpl. intuition. app equivalenceS.
  rwi in_class_related H3. nin H3. ee. assert (A = x0). rwi inc_quotient H0.
  nin (class_dichot H0 H3). am. red in H6. elim (emptyset_pr (x:=x)).
  wr H6. app intersection2_inc. rw H1. fprops. am.
  wri H6 H5; rwi H1 H5; db_tac. am.
  ir. nin H0. nin H0. split. rw inc_quotient. red. 
  assert (inc x E). ap H. rw H0. fprops.
  assert (rep A = x).  assert (nonempty A). exists x. rw H0. fprops. 
  cp (nonempty_rep H3). rewrite H0 in H4. cp (singleton_eq H4). ue. rw H3.
  split. am. split. rw substrate_Sgraph.  am.
  set_extens.  bw. rwi H0 H4. rw (singleton_eq H4). wri substrate_Sgraph H2.
  equiv_tac.
  bwi H4.
  assert (related Sgraph x0 x). equiv_tac.
  ufi Sgraph H5. rwi graph_on_rw2 H5. nin H5. nin H5. nin H6.
  assert (forall c, chained_r c -> chain_tail c = x -> chain_head c = x). ir.
  induction c; simpl in *. rwi H9 H8. sy. app H1. app A2.
  nin H8. rwi IHc H8.  sy. app H1. app A2. am.
  am. rwi (H8 _ H5 H7) H6. rw H0.  rw H6. fprops. ap equivalenceS. am. am.
  red. exists x. am.
Qed.

Definition is_constituant A :=
  (exists a, A = singleton a & inc a E & forall b, R a b -> a = b) \/
  (exists a, exists b, A = Cab a b& a<> b & R a b).

Lemma constituant_inter2 : forall A B,
  is_constituant A -> is_constituant B -> intransitive1 ->
  A = B \/ small_set (intersection2 A B).
Proof. ir. red in H; red in H0. nin H. right. nin H. nin H. rw H. red. ir. 
  cp (intersection2_first H3). cp (intersection2_first H4). 
  rw (singleton_eq H5). db_tac.
  nin H0. nin H0. nin H0. right. rw H0. red. ir. 
  cp (intersection2_second H3). cp (intersection2_second H4). 
  rw (singleton_eq H5). db_tac.
  nin H. nin H. nin H0. nin H0. nin (equal_or_not A B). left. tv.
  right. red. ir. ee. nin (equal_or_not u v). am. 
  nin (intersection2_both H3). nin(intersection2_both H4). 
  rwi H H10; rwi H H12. cp (Cab_trans H7 H8 H1 H9 H10 H12).
  rwi H0 H11; rwi H0 H13. cp (Cab_trans H5 H6 H1 H9 H11 H13).
  elim H2. ue. ue. ue. 
Qed.

Lemma constitutant_inter3 : forall A B C,
  is_constituant A -> is_constituant B -> is_constituant C ->  intransitive1 ->
  A = B \/ A = C \/ B = C \/  intersection2 A B = emptyset
  \/ intersection2 A C = emptyset \/ intersection2 B C = emptyset
  \/ (intersection2 A B = intersection2 A C  &
      intersection2 B C =  intersection2 A C).
Proof. ir. nin (equal_or_not A B). left. tv. right.
  nin (equal_or_not A C). left. tv. right.
  nin (equal_or_not B C). left. tv. right. 
  nin H.  nin H. ee. nin H0. nin H0. ee. left. app disjoint_pr.
  ir. rwi H H10. awi H10. rwi H0 H11. awi H11. elim H3. ue. ue.
  wr H10; wrr H11.
  nin H0. nin H0. ee. left.  app disjoint_pr. ir.  rwi H H10. awi H10.
  rwi H10 H11.  rwi H0 H11. ufi Cab H11. Ztac. elim H8.
  ee. wr (H7 _  (A2 H13)). wr (H7 _  (A2 H14)). tv.
  nin H0. nin H0. ee. right. right. nin H1. nin H1. ee. left.
  app disjoint_pr. ir. rwi H0 H10. awi H10. rwi H1 H11. awi H11.
  elim H5. ue. ue. wr H10. ue.
  nin H1. nin H1. left.  app disjoint_pr. ir. rwi H0 H8. awi H8. ee.
  rwi H8 H9. rwi H1 H9. ufi Cab H9. Ztac. ee. elim H10.
  wr (H7 _ (A2 H13)). wr (H7 _ (A2 H14)). tv.
  nin H1. nin H1. right. right. left. ap disjoint_pr. ir.
  ee. rwi H1 H7. awi H7. rwi H7 H6. nin H0. nin H0.  ee. rwi H0 H6.
  ufi Cab H6. Ztac. ee. elim H10.
  wr (H9 _ (A2 H13)). wr (H9 _  (A2 H14)). tv.
  nin (emptyset_dichot (intersection2 A B)). left. tv. right.
  nin (emptyset_dichot (intersection2 A C)). left. tv. right.
  nin (emptyset_dichot (intersection2 B C)). left. tv. right.
  nin H; nin H0; nin H1. nin H; nin H0; nin H1. nin H; nin H0; nin H1.
  nin H9; nin H10; nin H11. nin H6; nin H7; nin H8.
  nin (intersection2_both H6).
  nin (intersection2_both H7).
  nin (intersection2_both H8).
  rwi H H15; rwi H H17; rwi H0 H16; rwi H0 H19; rwi H1 H18; rwi H1 H20.
  unfold Cab in *. Ztac. clear H20. Ztac. clear H19.
  Ztac. clear H18. Ztac. clear H17. Ztac. clear H16. Ztac. clear H15. 
  set (job:=intersection2 A B = intersection2 A C &
   intersection2 B C = intersection2 A C). ee.
  assert (small_set (intersection2 A B)). assert (is_constituant A). red.
  right. exists x. exists x2. intuition. assert (is_constituant B). red.
  right. exists x0. exists x3. intuition. nin (constituant_inter2 H33 H34 H2).
  elim H3. tv. am.
  assert (small_set (intersection2 A C)). assert (is_constituant A). red.
  right. exists x. exists x2. intuition. assert (is_constituant C). red.
  right. exists x1. exists x4. intuition. nin (constituant_inter2 H34 H35 H2).
  elim H4. tv. am.  
  assert (small_set (intersection2 B C)). assert (is_constituant C). red.
  right. exists x1. exists x4. intuition. assert (is_constituant B). red.
  right. exists x0. exists x3. intuition. nin (constituant_inter2 H36 H35 H2).
  elim H5. tv. am. 
  cp (H2 _ _ _ _ H9 H12 H15 H25 H27 H29).
  cp (H2 _ _ _ _ H10 H13 H26 H23 H28 H31).
  cp (H2 _ _ _ _ H11 H14 H22 H24 H32 H30).
  assert (y= y0). nin (equal_or_not y y0). am.
  cp (H2 _ _ _ _ H39 H36 (A2 H15) H37 (A2 H25) (A2 H38)).
  cp (H2 _ _ _ _ H39 H36 (A2 H27) H37 (A2 H29) (A2 H38)).
  assert (inc y1 A). rw H. uf Cab. Ztac. 
  assert (inc y1 (intersection2 A C)). app intersection2_inc.
  ap (intersection2_second H8). cp (H34 _ _ H43 H7).
  assert (inc y1 (intersection2 A B)). app intersection2_inc.
  ap (intersection2_first H8). cp (H33 _ _ H45 H6).  wrr H46.
  assert (y = y1).  assert (inc y (intersection2 B C)).
  app intersection2_inc. app (intersection2_second H6). rw H39.
  app (intersection2_second H7). cp (H35 _ _ H40 H8). tv.
  split. set_extens. rw (H33 _ _ H41 H6). rww H39. rw (H34 _ _ H41 H7). ue.
  set_extens. rw (H35 _ _ H41 H8). wr H40; ue. rw (H34 _ _ H41 H7).
  wr H39. ue.
Qed.

End Exercice6_10.

Definition exercise6_11b_assumption X E:=
  union X = E 
  & (forall A, inc A X -> nonempty A)
  & (forall A B, inc A X -> inc B X -> A = B \/ small_set (intersection2 A B))
  & (forall A B C, inc A X -> inc B X -> inc C X -> 
    ( A=B \/ A = C \/ B = C \/ intersection2 A B = emptyset 
      \/ intersection2 A C = emptyset 
      \/ intersection2 B C = emptyset 
      \/ (intersection2 A B = intersection2 A C &
      intersection2 A B = intersection2 B C))).
Definition exercise6_11b_rel X x y := exists A, inc A X & inc x A & inc y A.

Lemma exercise6_11b1: forall E X,
  exercise6_11b_assumption X E -> reflexive_r (exercise6_11b_rel X) E.
Proof. ir. red. ir. app iff_eq. ir. red. red in H. ee. wri H H0. 
  nin (union_exists H0). exists x. intuition. ir. red in H0. nin H0.
  nin H0. nin H. wr H. nin H1. ap (union_inc H1 H0).
Qed.

Lemma exercise6_11b2: forall E X,
  exercise6_11b_assumption X E -> symmetric_r (exercise6_11b_rel X).
Proof. ir. red. uf exercise6_11b_rel.  ir. nin H0. exists x0. intuition.
Qed.

Lemma exercise6_11b3: forall E X, exercise6_11b_assumption X E -> 
  let R := exercise6_11b_rel X in
    forall  x y z t,  
      x <> y ->  x<>z -> x <> t -> y <> z -> y <> t -> z <> t ->
      R x y -> R x z -> R x t -> R y z -> R y t -> R z t.
Proof. ir. unfold R in *.  unfold exercise6_11b_rel in *.  
  nin H6; nin H7; nin H8; nin H9; nin H10. ee.
  nin (equal_or_not x1 x2). exists x1. intuition. ue.
  nin (equal_or_not x1 x4). exists x1. intuition. ue.
  nin (equal_or_not x3 x2). exists x3. intuition. ue.
  nin (equal_or_not x3 x4). exists x3. intuition. ue.
  assert (intersection2 x1 x2 = singleton x). set_extens.
  assert (inc x (intersection2 x1 x2)). app intersection2_inc.
  red in H. ee. nin (H28 _ _ H7 H8). contradiction. rw (H30 _ _ H25 H26). 
  fprops. rw (singleton_eq H25). app intersection2_inc.
  assert (intersection2 x3 x4 = singleton y). set_extens.
  assert (inc y (intersection2 x3 x4)). app intersection2_inc.
  red in H. ee. nin (H29 _ _ H9 H10). contradiction.
  rw (H31 _ _ H26 H27). fprops. rw (singleton_eq H26). app intersection2_inc.
  nin (equal_or_not x0 x1).
  assert (x0 = x3).
  assert (inc y (intersection2 x0 x3)). app intersection2_inc.
  assert (inc z (intersection2 x0 x3)). wri H27 H18. app intersection2_inc.
  red in H; ee. nin (H31 _ _ H6 H9). am. elim H3. ap (H33 _ _ H28 H29). 
  nin (equal_or_not x0 x4). exists x0. wri H27 H18. wri H29 H12. intuition. 
  nin (equal_or_not x2 x4). 
  assert (inc x (intersection2 x0 x2)). app intersection2_inc.
  assert (inc y (intersection2 x0 x2)). app intersection2_inc. rww H30.
  red in H; ee. nin (H34 _ _ H6 H8). exists x3. intuition. wr H28. rww H36.
  elim H0. ap (H36 _ _ H31 H32). 
  wri H27 H21.
  red in H. ee. nin (H33 _ _ _ H6 H8 H10). contradiction. nin H34.
  contradiction. nin H34. contradiction.
  assert (inc x (intersection2 x0 x2)). app intersection2_inc. 
  assert (inc y (intersection2 x0 x4)). app intersection2_inc. 
  assert (inc t (intersection2 x2 x4)). app intersection2_inc.  
  nin H34. rwi H34 H35. elim (emptyset_pr H35). nin H34. 
  rwi H34 H36. elim (emptyset_pr H36). nin H34. rwi H34 H37. 
  elim (emptyset_pr H37). exists x3. intuition. wr H28. wri H39 H37.
  app (intersection2_first H37).
  ir. assert (intersection2 x0 x1 = singleton x).
  assert (inc x (intersection2 x0 x1)). app intersection2_inc.
  red in H. ee. nin (H30 _ _ H6 H7).  contradiction. red in H32. set_extens.
  rw (H32 _ _ H28 H33). fprops. rw (singleton_eq H33). am.
  nin (equal_or_not x1 x3). assert (inc y (singleton x)).
  wr H28. app intersection2_inc. rww H29. elim H0. rww (singleton_eq H30). 
  assert (intersection2 x1 x3 = singleton z).
  assert (inc z (intersection2 x1 x3)). app intersection2_inc.
  red in H. ee. nin (H32 _ _ H7 H9). contradiction.  red in H34. set_extens.
  rw (H34 _ _ H30 H35). fprops. rw (singleton_eq H35). am.
  ir.
  nin (equal_or_not x0 x4). 
  assert (x0 = x2).
  assert (inc x (intersection2 x0 x2)). app intersection2_inc.
  assert (inc t (intersection2 x0 x2)). rw H31. app intersection2_inc.
  red in H; ee. nin (H35 _ _ H6 H8). am. cp (H37 _ _ H32 H33). elim H2. am.
  nin (equal_or_not x0 x3). ir. exists x0. wri H33 H14.  wri H31 H12. intuition.
  assert (inc x (intersection2 x0 x1)). app intersection2_inc. 
  assert (inc y (intersection2 x0 x3)). app intersection2_inc. 
  assert (inc z (intersection2 x1 x3)). app intersection2_inc.  
  nin H. ee. cp (H39 _ _ _ H6 H7 H9).  nin H40. contradiction. nin H40. 
  elim H33. am. nin H40. elim H29. am. nin H40.
  rwi H40 H34. elim (emptyset_pr H34). nin H40. rwi H40 H35. 
  elim (emptyset_pr H35). nin H40. rwi H40 H36. 
  elim (emptyset_pr H36). exists x2. intuition. wr H32. wri H42 H36.
  app (intersection2_first H36).
  ir. assert (intersection2 x0 x4 = singleton y).
  assert (inc y (intersection2 x0 x4)). app intersection2_inc.
  red in H. ee. nin (H34 _ _ H6 H10). elim H31. tv. red in H36. set_extens.
  rw (H36 _ _ H32 H37). fprops. rw (singleton_eq H37). am.
  nin (equal_or_not x2 x4). assert (inc x (singleton y)).
  wr H32. app intersection2_inc. wrr H33. elim H0. rww (singleton_eq H34). 
  ir.  assert (intersection2 x2 x4 = singleton t).
  assert (inc t (intersection2 x2 x4)). app intersection2_inc.
  red in H. ee. nin (H36 _ _ H8 H10). elim H33. tv. red in H38. set_extens.
  rw (H38 _ _ H34 H39). fprops. rw (singleton_eq H39). am.
  nin (equal_or_not x0 x2). nin (equal_or_not x0 x3).
  elim H23. wr H35; wr H36; tv. nin H; ee. cp (H39 _ _ _ H6 H7 H9).
  nin H40. elim H27. am. nin H40. elim H36. am. nin H40. elim H29. am.
  nin H40. assert (inc x emptyset).  wr H40. rw H28. fprops. 
  elim (emptyset_pr  H41). nin H40. assert (inc y emptyset). wr H40.
  app intersection2_inc. elim (emptyset_pr H41). nin H40.
  assert (inc z emptyset). wr H40. app intersection2_inc. 
  elim (emptyset_pr H41). nin H40.  rwi H28 H41. rwi H30 H41.
  elim H1. app (singleton_inj H41). 
  nin H. ee. cp (H38 _ _ _ H6 H8 H10).
  nin H39. elim H35. am. nin H39. elim H31. am. nin H39. elim H33. am.
  nin H39. assert (inc x emptyset).  wr H39.  app intersection2_inc.
  elim (emptyset_pr  H40). nin H39. assert (inc y emptyset). wr H39.
  app intersection2_inc. elim (emptyset_pr H40). nin H39.
  assert (inc t emptyset). wr H39. app intersection2_inc. 
  elim (emptyset_pr H40). nin H39.  rwi H39 H40. rwi H32 H40. rwi H34 H40.
  elim H4. app (singleton_inj H40). 
Qed.

Lemma exercise6_11b4: forall E X, exercise6_11b_assumption X E -> 
  let R := exercise6_11b_rel X in
    let p1 := fun u => (exists a, exists b, a<> b & R a b & u = 
      Zo E (fun x => R a x & R b x)) in
    let p2:= fun u => (exists x, u = singleton x & inc x E&
      forall y, inc y E -> R x y -> x = y) in
    let p3:= fun u => (exists v, inc v X & u <> v & sub u v & is_singleton u) in
      (forall u, inc u X -> p1 u \/ p2 u \/ p3 u ) &
      (forall u, p1 u -> inc u X) & (forall u, p2 u -> inc u X).
Proof. ir. split. ir. nin (p_or_not_p (is_singleton u)). ir. right. 
  nin (p_or_not_p (p3 u)). ir. right. tv. ir. left. red in H1. nin H1. 
  exists x. split. am. split. red in H. ee. wr H. apply union_inc with  u.
  rw H1. fprops.  am. ir. red in H4. red in H4. nin H4. 
  nin (equal_or_not x y). tv. ir.
  elim H2. exists x0. ee. am. rw H1. red. ir. elim H5. wri H8 H7.
  db_tac.  rw H1. red. ir. db_tac. red.
  exists x. tv. 
  ir. left. red in H. ee. nin (H2 _ H0). exists y.
  nin (p_or_not_p (exists v, inc v u & v <> y)). ir. nin H6. nin H6.
  exists x. split. auto. split. red. red. exists u. auto. set_extens.
  Ztac. wr H. apply union_inc with u. am. am. split. red. red. exists u.
  intuition. red. red. exists u. intuition. Ztac. ee. nin H10. nin H11. ee.
  nin (equal_or_not x1 u). wrr H16. nin (equal_or_not x2 u). wrr H17.
  assert (inc x (intersection2 u x2)). app intersection2_inc.
  assert (inc y (intersection2 u x1)). app intersection2_inc.
  nin (equal_or_not x1 x2). 
  nin (H3 _ _ H0 H10). elim H16. sy. am. red in H21. wri H20 H18.
  elim H7. app H21. ir. cp (H4 _ _ _ H0 H10 H11). nin H21. elim H16. sy; am.
  nin H21. elim H17. sy; am. nin H21. elim H20. am. nin H21. 
  assert (inc y emptyset). wr H21. app intersection2_inc.
  elim (emptyset_pr H22). nin H21. assert (inc x emptyset).  wr H21.
  app intersection2_inc. elim (emptyset_pr H22). nin H21. 
  assert (inc x0 emptyset).  wr H21.
  app intersection2_inc. elim (emptyset_pr H22). nin H21. 
  nin (H3 _ _ H0 H10). elim H16. sy. am. red in H23. wri H21 H18.
  elim H7. app H23. 
  ir. elim H1. red. exists y.  set_extens. nin (equal_or_not x y).
  rw H8. fprops. ir. elim H6. exists x. split; am. db_tac.
  split. ir. nin H0. nin H0; nin H0. ee. nin H. ee. red in H1. red in H1. 
  nin H1. ee. 
  assert (u = x1).  rw H2. set_extens.  Ztac.  ee.
  nin H10. nin H10. nin H12. nin H11. nin H11. nin H14.
  nin (equal_or_not x1 x3). rww H16. nin (equal_or_not x1 x4). rww H17.
  assert (inc x (intersection2 x1 x3)). app intersection2_inc.
  assert (inc x0 (intersection2 x1 x4)). app intersection2_inc.
  nin (equal_or_not x3 x4).
  nin (H4 _ _ H1 H10). elim H16. am. red in H21. wri H20 H19.
  elim H0. app H21. ir. cp (H5 _ _ _ H1 H10 H11). nin H21. elim H16. am.
  nin H21. elim H17. am. nin H21. elim H20. am. nin H21. 
  assert (inc x emptyset). wr H21. app intersection2_inc.
  elim (emptyset_pr H22). nin H21. assert (inc x0 emptyset).  wr H21.
  app intersection2_inc. elim (emptyset_pr H22). nin H21. 
  assert (inc x2 emptyset).  wr H21.
  app intersection2_inc. elim (emptyset_pr H22). nin H21. 
  nin (H4 _ _ H1 H10). elim H16. am. red in H23. wri H21 H19.
  elim H0. app H23. 
  Ztac. wr H. apply union_inc with x1. am. am. split. red; red.  exists x1.
  intuition. red. red. exists x1. intuition. rw H8. am.
  ir. red in H0. nin H0. ee. red in H. ee. wri H H1. cp (union_exists H1).
  nin H6. nin H6. assert (u = x0). set_extens. rwi H0 H8. 
  rw (singleton_eq H8). am. assert (inc x1 E). wr H. apply union_inc with x0.
  am. am. assert (R x x1). red. red. exists x0. intuition. wr (H2 _ H9 H10).
  rw H0. fprops. rww H8.
Qed.

End Exercice1.