(** * Theory of Sets  EII-6 Equivalence relations
  Copyright INRIA (2009-2013) Apics; Marelle Team (Jose Grimm).
  Part of this code comes from Carlos Simpson 
*)
(* $Id: sset4.v,v 1.48 2016/05/18 14:54:53 grimm Exp $ *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset3.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


(** ** EII-6-1 Definition of an equivalence relation *)

Module Relation.

(** the substrate of a relation are elements that are relate *)

Definition substrate r :=  (domain r) \cup (range r).

Lemma pr1_sr r y:
  inc y r -> inc (P y) (substrate r).
Proof. move => yr; apply: setU2_1; apply/funI_P; ex_tac. Qed.

Lemma pr2_sr r y:
  inc y r -> inc (Q y) (substrate r).
Proof. move => yr; apply: setU2_2; apply/funI_P; ex_tac. Qed.

Lemma arg1_sr r x y:
  related r x y -> inc x (substrate r).
Proof. by move=> rel; rewrite -(pr1_pair x y); apply: pr1_sr.  Qed.

Lemma arg2_sr r x y:
  related r x y -> inc y (substrate r).
Proof. by move=> rel;rewrite -(pr2_pair x y); apply: pr2_sr. Qed.

Ltac substr_tac := 
  match  goal with 
    | H:inc ?x ?r |- inc (P ?x) (substrate ?r) 
      => apply: (pr1_sr H)
    | H:inc ?x ?r |- inc (Q ?x) (substrate ?r) 
      => apply: (pr2_sr H)
    | H:related ?r ?x _ |- inc ?x (substrate ?r)
      => apply: (arg1_sr H)
    | H:related ?r _ ?y |- inc ?y (substrate ?r) 
      => apply: (arg2_sr H)
    | H:inc(J ?x _ ) ?r|- inc ?x (substrate ?r) 
      => apply: (arg1_sr H)
    | H: inc (J _ ?y) ?r |- inc ?y (substrate ?r) 
      => apply: (arg2_sr H)
  end.

Lemma substrate_smallest r s:
  (forall y, inc y r -> inc (P y) s) ->
  (forall y, inc y r -> inc (Q y) s) ->
  sub (substrate r) s.
Proof. move=> h1 h2 x; case /setU2_P; move/funI_P => [z zr ->]; fprops. Qed.

Lemma substrate_P r:  sgraph r -> forall x,
  inc x (substrate r) <-> 
      ((exists y, inc (J x y) r) \/  (exists y, inc (J y x) r)).
Proof.  
move => gr x; split; last by case => [] [y yr]; substr_tac.
by case /setU2_P => /funI_P [z zr ->]; [left | right]; ex_tac; rewrite gr.  
Qed.

(** Reflexivity etc. properties for a relation *)

Section Definitions.
Implicit Type  (r: relation).

Definition reflexive_re r E :=
  forall x, inc x E <-> r x x.

Definition reflexive_rr r :=
  forall x y, r x y -> (r x x /\  r y y).

Definition equivalence_r r :=
  symmetric_r r /\ transitive_r r.

Definition equivalence_re r E :=
  equivalence_r r /\ reflexive_re r E.

Definition order_r r :=
  [/\ transitive_r r,  antisymmetric_r r & reflexive_rr r].

Definition preorder_r r :=
  transitive_r r /\ reflexive_rr r.

Definition order_re  (r: relation)  x :=
  order_r r /\ reflexive_re r x.

End Definitions.

(** Same definitions for a graph *)

Definition reflexivep r :=  forall y, inc y (substrate r) -> related r y y.
Definition symmetricp r := symmetric_r (related r).
Definition antisymmetricp r := antisymmetric_r (related r).
Definition transitivep r :=  transitive_r (related r).

Definition equivalence r :=
  [/\ sgraph r, reflexivep r, transitivep r & symmetricp r].

Definition order r :=
  [/\ sgraph r, reflexivep r, transitivep r & antisymmetricp r].

Definition preorder r :=
  [/\ sgraph r, reflexivep r & transitivep r].

Definition order_on r E := order r /\ substrate r = E.
Definition equivalence_on r E := equivalence r /\ substrate r = E.


(** Basic properties *)

Lemma equivalence_sgraph  r: equivalence r -> sgraph r.
Proof. by move=>  []. Qed.

Lemma order_sgraph r: order r -> sgraph r.
Proof. by move => []. Qed.

Lemma preorder_sgraph r: preorder r -> sgraph r.
Proof. by move => []. Qed.

Hint Resolve order_sgraph equivalence_sgraph : fprops.

Lemma reflexive_domain g: reflexivep g -> domain g = substrate g.
Proof. 
move=> pb; set_extens u; first by apply: setU2_1.
case /setU2_P => // ug; apply/funI_P; exists (J u u);aw.
exact:(pb _  (setU2_2 (domain g) ug)).
Qed.

Lemma domain_sr g: equivalence g -> domain g = substrate g.
Proof. move=> h; apply: (reflexive_domain (proj42 h)). Qed.


Lemma domain_sr1 r: order r -> domain r = substrate r.
Proof.  move=> h; apply: (reflexive_domain (proj42 h)). Qed.

Lemma substrate_sub: {compat substrate : x y / sub x y}.
Proof. 
move => r s rs; move: (domain_S rs) (range_S rs) => pa pb t.
case /setU2_P => h; apply/setU2_P; fprops.
Qed. 

Lemma symmetric_transitive_equivalence r:
  sgraph r -> symmetricp r -> transitivep r -> equivalence r.
Proof. 
move=> gr sr tr; hnf; split => //.
move => y /(substrate_P gr) [][z pr].
   apply: (tr _ _ _ pr (sr _ _ pr)).
apply: (tr _ _ _  (sr _ _ pr) pr).
Qed. 

Lemma equivalence_relation_pr1 g:
  sgraph g -> equivalence_r (related g)  -> equivalence g.
Proof.
move=> gg [sr tr]; apply: symmetric_transitive_equivalence => //.
Qed.

Lemma reflexivity_e r u:
  equivalence r -> inc u (substrate r) -> related r u u.
Proof. by  move=> er us; apply:(proj42 er). Qed.

Lemma symmetricity_e r u v:
  equivalence r -> related r u v -> related r v u.
Proof. by move=> /proj44; apply. Qed.

Lemma transitivity_e  r v u w:
  equivalence r ->  related r u v -> related r v w -> related r u w.
Proof.
move=> er r1 r2; apply: ((proj43 er) _ _ _ r1 r2).
Qed.

Ltac equiv_tac:=
  match goal with 
    | H: equivalence ?r, H1: inc ?u (substrate ?r) |- related ?r ?u ?u
      => apply: (reflexivity_e H H1) 
    | H: equivalence ?r |- inc (J ?u ?u) ?r
      => apply: reflexivity_e
    | H:equivalence ?r, H1:related ?r ?u ?v |- related ?r ?v ?u
      => apply: (symmetricity_e H H1)
    | H:equivalence ?r, H1: inc (J ?u ?v) ?r |- inc (J ?v ?u) ?r
      => apply: (symmetricity_e H H1)
    | H:equivalence ?r, H1:related ?r ?u ?v, H2: related ?r ?v ?w
      |- related ?r ?u ?w
      => apply: (transitivity_e H H1 H2)
    | H:equivalence ?r, H1:related ?r ?v ?u, H2: related ?r ?v ?w
      |- related ?r ?u ?w
      => apply: (transitivity_e H (symmetricity_e H H1) H2)
    | H:equivalence ?r, H1:related ?r ?u ?v, H2: related ?r ?w ?v
      |- related ?r ?u ?w
      => apply: (transitivity_e H H1 (symmetricity_e H H2))
    | H: equivalence ?r, H1: inc (J ?u ?v) ?r, H2: inc (J ?v ?w) ?r |-
      inc (J ?u ?w) ?r
      => apply: (transitivity_e H H1 H2)
end.



(** Comparison of the two sets of definitions *)

Lemma equivalence_equivalence r:
  equivalence r -> equivalence_re (related r)(substrate r).
Proof. 
move => [gr ra rb rc]; split => // y.
by split => p; [ apply: ra | substr_tac ].
Qed.

(** We say that [g] is the graph of [r] if [related g] is the same function 
as [r]. We define the graph of [r] on [x] as the set of pairs of [x] related
 by [r] *)

Definition graph_on (r:relation) x:= 
  Zo(coarse x)(fun w => r (P w)(Q w)).

Lemma graph_on_graph r x: sgraph (graph_on r x).
Proof. by move => y /Zo_S /setX_P [ok _].  Qed.

Lemma graph_on_P0 r x a b:
  inc (J a b) (graph_on r x) <-> [/\ inc a x, inc b x & r a b].
Proof. 
split; first by move/Zo_P => [] /setX_P; aw ; move => [pa pb pc] pd;split.
move => [pa pb pc]; apply: Zo_i; [by apply: setXp_i | aw].
Qed.

Lemma graph_on_P1 r x a b:
  related (graph_on r x) a b <->  [/\ inc a x, inc b x & r a b].
Proof. apply/graph_on_P0. Qed.

Lemma graph_on_P2 r x : equivalence_re r x -> forall u v,
  (related (graph_on r x) u v <-> r u v).
Proof.
move=> [[rs rt] rr] u v; split; first by move/Zo_hi; aw.
move => ruv; apply/ graph_on_P1.
move: (rs _ _ ruv) => rvu; move: (rt _ _ _ ruv rvu) => ruu.
by move: (rt _ _ _ rvu ruv) => rvv; split => //; apply rr.
Qed.

Lemma graph_on_P3 r x:  order_re r x -> forall u v,
  (related (graph_on r x) u v <-> r u v).
Proof.
move=> [[_ _ cc] rr]; split; first by move /Zo_hi; aw.
move => ruv; move: (cc _ _ ruv) => [ruu rvv]. 
apply: Zo_i ; [by  apply:setXp_i; apply /rr |  aw].
Qed.

Lemma graph_on_sr1 r x:  sub (substrate (graph_on r x)) x.
Proof. 
by move=> y /(substrate_P (@graph_on_graph r x))[] [z] /graph_on_P0 [pa pb _].
Qed.

Lemma order_preorder r: order r -> preorder r.
Proof. by move => [gr tr ar rr]. Qed.

Lemma preorder_from_rel r x:
  preorder_r r -> preorder (graph_on r x).
Proof. 
move=> pr.
have gg: sgraph (graph_on r x) by apply: graph_on_graph.
move: pr=> [tr rr].
split=>//.
  by move=> y /(substrate_P gg) [] [z] /graph_on_P0 [yx zx ryz];
   apply /graph_on_P0; split => // ;move: (rr _ _ ryz) => [].
move=> a b c /graph_on_P1 [ax bx rab] /graph_on_P1 [_ cx rbc].
apply /graph_on_P1;split => //; apply: tr rab rbc.
Qed.

Lemma order_from_rel r x: order_r r -> order (graph_on r x).
Proof.
move=> [ta tb tc].
have [tr pa pb]: preorder (graph_on r x) by apply: preorder_from_rel; split.
split => //.
by move=> a b /graph_on_P1 [ax bx rab] /graph_on_P1 [_ _ rba]; apply: tb.
Qed.

Lemma equivalence_from_rel r x:
  equivalence_r r -> equivalence (graph_on r x).
Proof.
move=> [pa pb].
have gg: sgraph (graph_on r x) by apply: graph_on_graph.
apply: (equivalence_relation_pr1 gg).
split.
   move => a b /graph_on_P1 [ax bx rab]; apply /graph_on_P1. 
   by split => //; apply: pa.
move=> a b c /graph_on_P1 [ax bx rab] /graph_on_P1 [_ cx rbc].
apply /graph_on_P1;split => //; apply: pb rab rbc.
Qed.

Lemma graph_on_sr (r: relation) x:
  (forall a, inc a x -> r a a) ->
  substrate (graph_on r x) = x.
Proof.
move=> rr.
apply: extensionality; first by apply: graph_on_sr1.
move => t xt; move: (rr _ xt) => rtt.
apply: (arg1_sr (y:=t)); apply: Zo_i; [by apply:setXp_i | aw].
Qed.

Hint Rewrite graph_on_sr: bw.

(** Finest relation on a set: an element is only related to itself 
 The correspondence is the identity, the graph is the diagonal *)

Definition restricted_eq x := fun u v => inc u x /\ u = v.

Lemma diagonal_graph_on x: graph_on (restricted_eq x) x = diagonal x.
Proof.
set_extens t. 
  move /Zo_P => [pa [pb pc]]; apply /diagonal_i_P;split=> //. 
  by move /setX_P: pa =>[].
move /diagonal_i_P=> [pa pb pc];apply/Zo_i => //; apply /setX_P; split => //;ue.
Qed.

Lemma diagonal_equivalence x: equivalence_on (diagonal x) x.
Proof.
rewrite -diagonal_graph_on; split; last by bw => t tx.
apply: equivalence_from_rel;split.
  by move=> a b /= [ax] <-.
by move=> a b c [au ab] [bu bc]; split =>//; ue.
Qed.

Lemma diagonal_osr x: order_on (diagonal x) x.
Proof.
rewrite -diagonal_graph_on; split; last by bw => t tx.
apply: order_from_rel;split.
- by move=> a b c [au ab] [bu bc]; split =>//; ue.
- by move=> a b /= [ax <-].
- by move=> a b [aa <-].  
Qed.

(** Example of an equivalence without graph: equipotency *)

Lemma equipotent_equivalence: equivalence_r equipotent.
Proof. 
split; first by move=> x y;apply: EqS. 
move => x y z; apply: EqT.
Qed.

(** The coarsest relation on a set: everything is related *)
 

Lemma coarse_related u x y:
  related (coarse u) x y <-> (inc x u /\ inc y u). 
Proof.
by split; [ move/setX_P => [_]; aw | move => [pa pb];apply : setXp_i ].
Qed. 

Lemma coarse_graph x: sgraph (coarse x).
Proof. apply: setX_graph. Qed.

Lemma coarse_equivalence  u:  equivalence_on (coarse u) u. 
Proof.
have sr: substrate (coarse u) = u.
  rewrite /coarse/substrate. 
  transitivity (u \cup u); last by apply: setU2_id.
  case: (emptyset_dichot u); [  move ->; rewrite setX_0l; bw | move=> h; bw ].
split; [split | exact].
- by apply: coarse_graph. 
- by move => y; rewrite sr => yu;apply/ coarse_related.
   move=> x y z /coarse_related [pa pb]/coarse_related [pc pd].
- by apply/coarse_related.
- by move=> x y /coarse_related  [pc pd]; apply/coarse_related.
Qed.

Lemma sub_graph_coarse_substrate r:
  sgraph r -> sub r (coarse (substrate r)).
Proof. 
rewrite /coarse=> gr t tr; apply: setX_i; first (by apply: gr); substr_tac. 
Qed.

(** Example 5 page E II.114 *)

Lemma equivalence_relation_bourbaki_ex5 A E
    (r := (fun x y => (inc x (E -s A) /\ (x = y) \/ (inc x A /\ inc y A)))):
    sub A E ->  equivalence_on (graph_on r E)  E.
Proof. 
move => sa; split; last first.
  apply: graph_on_sr; move => a ae.
  by case: (inc_or_not a A) => h; [right | left]; split => //; apply /setC_P.
apply: equivalence_from_rel; split.
  move=> x y; case=> [] [pa pb]; [left | right ]; split => //; ue.
move => y x z [] [pa pb]; first by rewrite pb.
move => h;right; case:h =>  [] [qa qb]; split => //; ue.
Qed.

(** Intersection of equivalence relations is an equivalence *)

Lemma setIrel_graph  z:
  (alls z sgraph) -> sgraph (intersection z).
Proof. 
case: (emptyset_dichot z).
   move => -> _; rewrite setI_0; apply: sgraph_set0.
move => [t tz] alg y yi; apply: (alg _ tz); exact: (setI_hi yi tz).
Qed.


Lemma setIrel_P z:  nonempty z -> forall x y,
  (related (intersection z) x y <->
    (forall r, inc r z -> related r x y)). 
Proof. move=> nez x y; apply/(setI_P nez). Qed.

Lemma setIrelR z:
  (alls z reflexivep) -> reflexivep (intersection z).
Proof.
move => alr.
case: (emptyset_dichot z).
   move => -> x; rewrite setI_0 /substrate domain_set0 range_set0.
   by case /setU2_P => /in_set0.
move => nez y ys; apply/(setIrel_P nez) => r rz; apply: (alr _ rz).
apply: (substrate_sub (setI_s1 rz) ys).
Qed.

Lemma setIrel_sr z e:
  nonempty z -> (alls z reflexivep) ->
  (forall r, inc r z -> substrate r = e) ->
  substrate (intersection z) = e.
Proof. 
move=> nez allr alls.
move: (setIrelR allr)=> ir. 
set_extens t => ts.
  move: (ir _ ts); rewrite /related=> aux.
  move: nez => [u uz]; move: (setI_hi aux uz) => Ju.
  by rewrite - (alls _ uz); apply: (arg1_sr Ju).
have rtt: related (intersection z) t t.
  apply/(setIrel_P nez) => r rz; rewrite - (alls _ rz) in ts. 
  by apply: (allr _ rz). 
substr_tac.
Qed.

Lemma setIrelT z:
  (alls z transitivep) -> transitivep (intersection z).
Proof. 
move=> allt; case: (emptyset_dichot z).
   move => ->; rewrite setI_0 => a b c;case; case.
move=> neX y x u /(setIrel_P neX) rxy /(setIrel_P neX) ryz. 
apply/(setIrel_P neX) => r rz. 
exact: ((allt _ rz) _ _ _ (rxy _ rz)  (ryz _ rz)).
Qed.


Lemma setIrelS z:
  (alls z symmetricp) -> symmetricp (intersection z).
Proof.
move=> alls; case: (emptyset_dichot z).
  move ->; rewrite setI_0 => a b; case; case.
move=>nez x y /(setIrel_P nez) rxy; apply/(setIrel_P nez) => r rz.
apply: ((alls _ rz) _ _ (rxy _ rz)).
Qed.

Lemma setIrel_equivalence z:
  (alls z equivalence) -> equivalence (intersection z).
Proof. 
move=> alleq; apply: symmetric_transitive_equivalence.
- by apply: setIrel_graph => r /alleq  []. 
- by apply: setIrelS=> // r /alleq [_ _]. 
- by apply: setIrelT=> // r /alleq [_ _ ]. 
Qed.

Lemma setIrel_or z: (alls z order) -> order (intersection z).
Proof. 
move=> alleq;split.
- by apply: setIrel_graph => r /alleq [].
- by apply: setIrelR => r /alleq [_ ].
- by apply: setIrelT=> //  r /alleq [_ _ ]. 
- case: (emptyset_dichot z).
    move => ->; rewrite setI_0 => a b; case; case.
  move => [t te] x y pa pb; move: (alleq _ te)=> [_ _ _]; apply.
    apply:(setI_hi pa te).
  apply:(setI_hi pb te).
Qed.

(** The set of all relations or all equivalences of a set *)

Definition equivalences x :=
  Zo (powerset (coarse x)) (equivalence_on ^~ x).


Lemma equivalencesP r x:
  inc r (equivalences x) <-> (equivalence_on r x).
Proof. 
split; first by move /Zo_hi. 
move => pa; apply:Zo_i => //; apply/setP_P.
move: pa => [[xx _ _ _] <-].
by move: (sub_graph_coarse_substrate xx). 
Qed. 

Lemma inc_coarse_all_equivalence_relations u:
  inc (coarse u) (equivalences u).
Proof. 
by apply/equivalencesP; apply: coarse_equivalence. 
Qed.

(** We show that an equivalence is a self-inverse projector *)

Lemma selfinverse_graph_symmetric r: sgraph r ->
  (symmetricp r <-> (r = inverse_graph r)).
Proof.
move => gr; split => sp; last by move => x y Jr; rewrite sp; apply/igraph_pP.
set_extens t => tr.
  move: (gr _ tr) => aux.
  by rewrite - aux; apply/igraph_pP; apply: sp; hnf; rewrite  aux.
by move /igraphP: tr => [pt pa]; rewrite -pt; apply: sp.
Qed.

Lemma idempotent_graph_transitive r:
  sgraph r -> (transitivep r <-> sub  (r \cg r) r).
Proof. 
move=> gr; split. 
  move=> tr t /compg_P [pt [y J1r J2r]].
  rewrite - pt; move: tr J1r J2r; apply.
by move => h x y z Jxy Jyz; apply: h; apply/compg_pP; exists x.
Qed.

Theorem equivalence_pr r:
  equivalence r  <-> ((r \cg r) = r /\  r = inverse_graph r).
Proof.
split => hyp. 
  move: (hyp) => [pa pb pc pd].
  split; last by apply /selfinverse_graph_symmetric.
  apply: extensionality.
    by apply /idempotent_graph_transitive.
  move=> x xr; move: (pa _ xr) => px.
  rewrite - px; apply /compg_pP; exists (P x); rewrite ? px //.
  equiv_tac =>//; substr_tac.
move: hyp=> [crr ri].
have gr: (sgraph r) by rewrite ri; fprops.
apply: symmetric_transitive_equivalence => //.
  by apply /selfinverse_graph_symmetric.
apply/idempotent_graph_transitive => //; rewrite crr; fprops.
Qed.


(** ** EII-6-2 Equivalence classes; quotient set *)

(** Equivalence associated to a function [f] by  [f x = f y] *)

Definition eq_rel_associated f x y := 
  [/\ inc x (source f), inc y (source f) & Vf f x = Vf f y].

Definition equivalence_associated f := 
   (inverse_graph (graph f)) \cg (graph f).

Section EquivalenceAssociated.
Variable (f: Set).
Hypothesis (ff : function f).

Lemma ea_graph_on: 
   graph_on (eq_rel_associated f) (source f) = equivalence_associated f.
Proof.
set_extens t. 
  move /Zo_P => [/setX_P[pe _ _] [pb pc pd]].
  rewrite - pe; apply /compg_pP; exists (Vf f (P t)) => //; first Wtac.
  apply/igraph_pP; rewrite pd; Wtac.
move/compg_P => [pt [z pa /igraph_pP pb]].
have pc: inc (P t) (source f) by Wtac.
have pd: inc (Q t) (source f) by Wtac.
apply: Zo_i; first by apply /setX_P.
by split => //; rewrite - (Vf_pr ff pa) - (Vf_pr ff pb).
Qed.

Lemma ea_relatedP x y:
  related (equivalence_associated f) x y <->
  [/\ inc x (source f), inc y (source f) & Vf f x = Vf f y].
Proof. 
rewrite - ea_graph_on; split; first by move/graph_on_P1 => [_ _].
by move =>[pa pb pc]; hnf; apply /graph_on_P1.
Qed.


Lemma graph_ea_equivalence:
  equivalence_on (equivalence_associated f) (source f).
Proof.
rewrite - ea_graph_on; split; last by rewrite graph_on_sr. 
apply: equivalence_from_rel; split.
  by move => a b [pa pb pc].
move => a b c [pa pb pc] [pd pe pf]; split  => //; ue.
Qed. 

End EquivalenceAssociated.

(** The class of [x] is the set of elements related to [x] *)

Definition class r x := fun_image (Zo r (fun z => P z = x)) Q.
Definition quotient r := fun_image (substrate r) (class r).
Definition classp r x := inc (rep x) (substrate r) /\ x = class r (rep x).

Section Class.
Variable (r:Set).
Hypothesis (er: equivalence r).

Lemma class_P x y:  inc y (class r x) <-> related r x y.
Proof. 
have gr: (sgraph r) by fprops.
rewrite /related; split.
  by move/funI_P => [z /Zo_P [pa <-] ->]; rewrite (gr _ pa).
move=> h; apply/funI_P; exists (J x y); [ apply: Zo_i |]; aw.
Qed.

Lemma class_is_im_of_singleton x: 
  class r x = im_of_singleton r x. 
Proof. 
set_extens t; first by move/class_P/dirim_set1_P.
by move/dirim_set1_P/class_P.
Qed.

Lemma sub_class_substrate x: sub (class r x) (substrate r).
Proof. move=> t /class_P rt; substr_tac. Qed.

Lemma class_eq1 u v:  related r u v -> class r u = class r v.
Proof. 
move=> ruv; set_extens x; move/class_P => h; apply/class_P; equiv_tac.
Qed.

Lemma class_eq2 u v: inc u (class r v) -> class r u = class r v.
Proof.
by move =>  pb; symmetry;apply: class_eq1; apply/class_P.
Qed.

Lemma setQ_ne x: inc x (quotient r) -> nonempty x.
Proof. 
by move/funI_P => [z zr ->]; exists z; apply/class_P; equiv_tac.
Qed.

Lemma setQ_repi x: inc x (quotient r) -> inc (rep x) x.
Proof. by move => /setQ_ne; apply: rep_i. Qed.

Lemma inc_class_setQ x:
  inc x (substrate r) -> inc (class r x) (quotient r).
Proof. move => ta; apply/funI_P; ex_tac. Qed.

Lemma class_class x: inc x (substrate r) -> classp r (class r x).
Proof. 
move=> xs; move: (setQ_repi (inc_class_setQ xs)) =>/class_P rxr.
by split =>//; [substr_tac | apply: class_eq1].
Qed.

Lemma setQ_P x: inc x (quotient r) <-> classp r x.
Proof. 
apply: (iff_trans (funI_P _ _ _)); split.
  by move => [z zs ->]; apply: class_class.
move => [pa pb]; ex_tac.
Qed.

Lemma class_rep x: inc x (quotient r) -> class r (rep x) = x.
Proof. by move /setQ_P => [_].  Qed. 

Lemma in_class_relatedP  y z:
  related r y z <-> (exists x, [/\ classp r x, inc y x & inc z x]).
Proof. 
split.
  move=> ryx;exists (class r y). 
  have ys: inc y (substrate r) by substr_tac.
  split; first (by apply: class_class); apply/class_P => //; equiv_tac.
move =>[w [ [_ ->]]] /class_P pb /class_P pc; equiv_tac.
Qed.

Lemma related_rep_in_class  x y:
  inc x (quotient r) -> inc y x -> related r (rep x) y.
Proof. 
move=> xq; move: (xq) =>/setQ_P cx yx; apply/in_class_relatedP; exists x.
split => //;by apply: setQ_repi.
Qed.

Lemma rep_in_class x: classp r x -> inc (rep x) x.
Proof. move /setQ_P; apply: setQ_repi. Qed.

Lemma rel_in_class x y: classp r x -> inc y x -> related r (rep x) y.
Proof. by move /setQ_P => xq yx; apply: related_rep_in_class. Qed.

Lemma sub_class_sr x: classp r x -> sub x (substrate r).
Proof. move => [pa ->]; apply: sub_class_substrate. Qed.

Lemma rel_in_class2 x y: classp r x -> related r (rep x) y -> inc y x.
Proof. by move => pa pb; rewrite (proj2 pa); apply /class_P. Qed.

Lemma class_dichot x y: classp r x -> classp r y -> disjointVeq x y.
Proof. 
move=> cx cy; mdi_tac xy.
move => u ux uy; case: xy.
move: (rel_in_class cx ux) => pa.
move: (rel_in_class cy uy) => pb.
rewrite (proj2 cx)  (proj2 cy); apply: class_eq1; equiv_tac.
Qed.

Lemma inc_in_setQ_sr x y:
  inc x y -> inc y (quotient r) -> inc x (substrate r).
Proof. 
move=> xy /setQ_P [pa pb]; apply: (@sub_class_substrate (rep y)); ue.
Qed.

Hint Resolve inc_class_setQ: fprops.

Lemma setU_setQ: union (quotient r) = substrate r. 
Proof.
set_extens t => ts. 
  move: (setU_hi ts) => [z tz zu]; apply: (inc_in_setQ_sr  tz zu).
apply: (@setU_i _ (class r t)); [ apply/class_P; equiv_tac | fprops].
Qed. 

Lemma rep_i_sr x:  inc x (quotient r) -> inc (rep x) (substrate r).
Proof. by move /setQ_P => [g _]. Qed.

Lemma inc_itself_class x: inc x (substrate r) ->  inc x (class r x).
Proof. move => xsr; apply/class_P; equiv_tac. Qed.

Lemma related_rep_class x: inc x (substrate r) -> related r x (rep (class r x)).
Proof. 
move=> xs.
suff: related r (rep (class r x)) x by move=> h; equiv_tac.
by apply: related_rep_in_class; fprops; apply: inc_itself_class.
Qed.
 
Lemma related_rr_P u v:
  inc u (quotient r) -> inc v (quotient r) ->
  (related r (rep u) (rep v) <-> (u = v)). 
Proof.
move => uq vq; split.
  move=> h; rewrite - (class_rep uq) -(class_rep vq).
  by apply: class_eq1. 
by move=> ->; apply: (reflexivity_e er); apply: rep_i_sr.
Qed.

Lemma related_equiv_P  u v:
  related r u v <->
   [/\ inc u (substrate r), inc v (substrate r) & class r u = class r v].
Proof.
split.
  by move=> ruv; split; [substr_tac | substr_tac| apply: class_eq1].
move=> [us vs cuv]. 
apply /class_P; rewrite cuv; by apply: inc_itself_class.
Qed.

Lemma is_class_pr x y:
  inc x y -> inc y (quotient r) -> y = class r x.
Proof. 
move=> xy yq.
have <-: class r (rep y) = y by apply: class_rep.
apply: class_eq1=>// ; apply: (related_rep_in_class  yq xy).
Qed.

End Class.

Hint Resolve rep_i_sr inc_itself_class inc_class_setQ : fprops.


(** Canonical projection on the quotient *)

Definition canon_proj r := Lf (class r) (substrate r) (quotient r).

Section CanonProj.
Variable (r:Set).
Hypothesis (er: equivalence r).

Lemma canon_proj_f : function (canon_proj r).
Proof. apply: lf_function => t ts /=; fprops. Qed.

Lemma canon_proj_s : source (canon_proj r) = substrate r.
Proof. rewrite /canon_proj; aw. Qed.

Lemma canon_proj_t : target (canon_proj r) = quotient r.
Proof. rewrite /canon_proj; aw. Qed.

Hint Rewrite canon_proj_s canon_proj_t: aw.
Hint Resolve canon_proj_f: fprops.

Lemma canon_proj_V x:
  inc x (substrate r) -> Vf (canon_proj r) x = class r x.
Proof. rewrite /canon_proj=> xs; aw => t ts /=; fprops.  Qed.

Hint Rewrite canon_proj_V : aw.

Lemma canon_proj_setQ_i  x:
  inc x (substrate r) -> inc (Vf (canon_proj r) x) (quotient r).
Proof. move=> xs; aw; fprops. Qed.

Lemma rel_gcp_P  x y:
  inc x (substrate r) -> inc y (quotient r) ->
  (inc (J x y) (graph (canon_proj r)) <-> inc x y).
Proof. 
move=> xs yq.
have fc: (function (canon_proj r)) by fprops. 
split => h.
  move: (Vf_pr fc h); aw => ->; apply/class_P => //; equiv_tac.
have: (y = Vf (canon_proj r) x).
  aw; move: (class_rep er yq) h => <- /(class_P er) rryx.
  by apply: class_eq1.
move=> ->; Wtac; aw.
Qed.

Lemma canon_proj_fs: surjection (canon_proj r).
Proof. 
split;[ fprops | move=> y; aw => yr; exists (rep y); fprops].
aw; [ by apply: class_rep | fprops ].
Qed.


Lemma sub_im_canon_proj_quotient a x:
  sub a (substrate r) ->
  inc x (Vfs (canon_proj r) a) ->
  inc x (quotient r).
Proof. 
move=> sas xi.
have fc:function (canon_proj r) by fprops. 
have sa: sub a (source (canon_proj r)) by aw.
move /(Vf_image_P fc sa): xi => [u ua ->]; aw; fprops.
Qed.


(** Criterion 55 of Bourbaki*)

Lemma related_e_P u v:
  related r u v <->
   [/\ inc u (source (canon_proj r)),
     inc v (source (canon_proj r)) & 
     Vf (canon_proj r) u = Vf (canon_proj r) v].
Proof. 
rewrite canon_proj_s.
split; first by move/(related_equiv_P er) => [us vs cuv]; aw.
move => [us vs h]; apply/(related_equiv_P er); split => //; move: h; aw.
Qed.

End CanonProj.


Hint Rewrite canon_proj_s canon_proj_t: aw.
Hint Resolve canon_proj_f: fprops.
Hint Rewrite canon_proj_V : aw.


(** The diagonal is the graph of equality *)

Lemma diagonal_class x u:
  inc u x -> class (diagonal x) u = singleton u.
Proof.
have h:= (proj1 (diagonal_equivalence x)).
move=> ux; apply: set1_pr; first by apply/(class_P h) /diagonal_pi_P.
by move => z /(class_P h) /diagonal_pi_P [_ ->].
Qed.
 
Lemma canon_proj_diagonal_fb x:
  bijection (canon_proj (diagonal x)).
Proof. 
have [h sr] :=(diagonal_equivalence x).
have cps:= (canon_proj_fs h).
split => //; split;first by fct_tac.
aw; move=> a b ax bx /=; aw.
move: ax bx;rewrite sr => ax bx.
rewrite ! diagonal_class //; apply:set1_inj.
Qed.

Lemma canon_proj_diagonal_fb_contra r:
  equivalence r ->  bijection (canon_proj r) -> 
  r = diagonal (substrate r).
Proof.
move => pa pb.
set_extens t; last first.
 by move /diagonal_i_P => [Px px qx]; rewrite -Px -qx; apply: reflexivity_e.
move => tr; move: (pa) => [sa _ _ _]; move: (sa _ tr) => pt.
have ptsr: inc (P t) (substrate r) by substr_tac.
have qtsr: inc (Q t) (substrate r) by substr_tac.
apply /diagonal_i_P; split => //.
move: (bij_inj pb); rewrite canon_proj_s => h; move: (h _ _  ptsr qtsr).
by aw; apply; apply: class_eq1 => //;rewrite /related pt.
Qed.

(** Relation associated to [P] in a product *)

Definition first_proj_eqr x y :=
  eq_rel_associated (first_proj (x \times  y)).

Definition first_proj_eq x y :=
  equivalence_associated (first_proj (x \times y)).

Lemma first_proj_equivalence x y:
  equivalence_on (first_proj_eq x y) (x \times y).
Proof. 
by move:(graph_ea_equivalence (first_proj_f (x\times y))); rewrite lf_source.
Qed.

Lemma first_proj_eq_related_P x y a b:
  related (first_proj_eq x y) a b <->
  [/\ inc a (x \times y), inc b (x \times y) & P a = P b].
Proof.
have ff: function (first_proj (x \times y)) by apply:first_proj_f.
split.
  move/(ea_relatedP ff); rewrite lf_source; move => [pa pb].
  by rewrite ! first_proj_V.
by move => [pa pb pc]; apply/(ea_relatedP ff);rewrite lf_source !first_proj_V.
Qed.

Lemma first_proj_classP x y:  nonempty y -> forall z,
  (classp (first_proj_eq x y) z <->
  exists2 u, inc u x & z = (singleton u) \times y).
Proof. 
move=> [y0 y0y].
case:(first_proj_equivalence x y).
set (r:=first_proj_eq x y) => er sr.
move => z; split.
  move => cz; move: (proj1 cz); rewrite sr; move /setX_P  => [sa sb sc].
  exists (P (rep z)) => //.
  set_extens t => ta.
     move: (rel_in_class er cz ta) => /first_proj_eq_related_P [qa qb qc].
     by move /setX_P: qb => [rq rb rc]; apply /indexedrP.
  rewrite (proj2 cz); apply /(class_P er); apply /first_proj_eq_related_P.
  move/indexedrP: ta => [pa pb pc]; split => //; apply /setX_P; split => //; ue.
move=> [u uz zp]; rewrite zp.
have nep: (nonempty (singleton u \times y)). 
  by exists (J u y0); apply: setXp_i; fprops.
move: (rep_i nep); set w:= rep _ => pa.
move /indexedrP: (pa) => [ra rb rc].
have wp: inc w (x \times y) by apply /setX_P;split => //; ue.
hnf; rewrite - /w; split; first by ue.
set_extens t.
  move /indexedrP => [sa sb sc]; apply /(class_P er).
  by apply /first_proj_eq_related_P;split; [exact | apply /setX_P |];rewrite sb.
move /(class_P er) =>  /first_proj_eq_related_P [_ /setX_P [qa qb qc] qd].
apply /indexedrP;split => //; ue.
Qed.


Lemma first_proj_equiv_proj x y:
  nonempty y->
  bijection (Lf (fun u => (singleton u) \times y)
    x (quotient (first_proj_eq x y))).
Proof. 
move=> ney.
set (f:=fun u => (singleton u) \times y).
set (g:= (Lf f x (quotient (first_proj_eq x y)))).
have efp:=(proj1 (first_proj_equivalence x y)).
have ta: lf_axiom f x (quotient (first_proj_eq x y)).
  move => u ux ; apply /(setQ_P efp) /(first_proj_classP _  ney); ex_tac.
rewrite /g; apply: lf_bijective => //.
  rewrite /f => u v ux vx sp. 
  apply: set1_inj; rewrite - (setX_domain (singleton u) ney). 
  by rewrite sp setX_domain.
move=>z /(setQ_P efp) /(first_proj_classP _ ney) [u ux ep]; ex_tac.
Qed.

Lemma sub_quotient_powerset r:
  equivalence r ->
  sub (quotient r) (powerset (substrate r)).
Proof.
by move=> er x /(setQ_P er) => cr; apply /setP_P; apply: sub_class_sr.
Qed.

Lemma partition_from_equivalence r:
  equivalence r ->
  partition_s (quotient r)(substrate r).
Proof. 
move=> er.
split; last by move=> t tq; apply: (setQ_ne er tq).
split; first by apply: setU_setQ.
by move=> a b /(setQ_P er) ca /(setQ_P er) cd;apply: (class_dichot er).
Qed.

(** Partition of a set and induced equivalence *)

Definition in_same_coset f x y:=
   exists i, [/\ inc i (source f) , inc x (Vf f i) & inc y (Vf f i)].

Definition partition_relation f x := 
  graph_on (in_same_coset f) x.

Section InSameCoset.
Variables (f x: Set).
Hypothesis (ff: function f).
Hypothesis fpa:  partition_w_fam (graph f) x. 

Lemma partition_inc_unique1 i j y:
  inc i (source f) -> inc y (Vf f i) ->
  inc j (source f) -> inc y (Vf f j) -> i = j.
Proof.
rewrite (proj33 ff) => p1 p2 p3 p4.
by rewrite -(cover_at_pr fpa p1 p2) - (cover_at_pr fpa p3 p4).
Qed.

Lemma isc_hi a b: (in_same_coset f a b) -> (inc a x /\ inc b x).
Proof.
move => [t [tsf p1 p2]]; rewrite (proj33 ff) in tsf.
rewrite -(proj33 fpa); split; union_tac.
Qed.

Lemma isc_rel_P a b:
  (related (partition_relation f x) a b <-> in_same_coset f a b).
Proof. 
move: fpa => [qa qb qc].
split; first by move /graph_on_P1 => [_ _].
by move => h; move: (isc_hi h) => [ax bx]; apply /graph_on_P1.
Qed.

Lemma isc_rel1P a b: inc a x -> inc b x ->
   ((in_same_coset f a b) <-> (cover_at (graph f) a = cover_at (graph f) b)).
Proof.
move => ax bx; split.
  move => [t [tsf pa pb]].
  rewrite (proj33 ff) in tsf.
  by rewrite(cover_at_pr fpa tsf pa) (cover_at_pr fpa tsf pb).
move => h. 
move: (cover_at_in fpa ax) (cover_at_in fpa bx); rewrite -h - (proj33 ff).
set s := (cover_at (graph f) a); move => [pa pb] [pc pd].
by exists s.
Qed.

Lemma isc_rel_sr: substrate (partition_relation f x) =  x.
Proof. by apply: graph_on_sr => a ax; apply /isc_rel1P. Qed.

Lemma isc_rel_equivalence:
  equivalence (partition_relation f x).
Proof. 
apply: equivalence_from_rel; split.
  by move => u v [i [isf Wx Wy]]; exists i.
move => b a c pa pb.
move: (isc_hi pa) (isc_hi pb) => [ax bx] [_ cx].
apply/(isc_rel1P ax cx). 
by move /(isc_rel1P ax bx): pa => ->; move /(isc_rel1P bx cx): pb => ->.
Qed.

Lemma isc_rel_class a:
  classp (partition_relation f x) a ->
  exists2 u, inc u (source f) & a = Vf f u.
Proof.
move=> [rs ac].
move: isc_rel_equivalence => ec.
rewrite isc_rel_sr in rs.
move: (cover_at_in fpa rs); set u := cover_at _ _;move => [pa pb].
rewrite ac /Vf (proj33 ff); ex_tac.
set_extens t. 
   move /(class_P ec) /isc_rel_P => h; move: (proj2 (isc_hi h)) => tx.
   by move: (cover_at_in fpa tx)=> []; move /(isc_rel1P rs tx): h => <-.
move => ts.
have tx: inc t x by rewrite - (proj33 fpa); union_tac.
apply /(class_P ec) /isc_rel_P /(isc_rel1P rs tx).
by symmetry; apply:(same_cover_at fpa rs ts). 
Qed.

Lemma isc_rel_class2 u:
  inc u (source f) -> nonempty (Vf f u) ->
  classp (partition_relation f x)  (Vf f u) .
Proof. 
move=> us neW.
move: isc_rel_equivalence => ec.
rewrite (proj33 ff) in us.
have sWx: (sub  (Vf f u) x) by rewrite -(proj33 fpa) => t tW; union_tac.
move: (rep_i neW) => rw;move: (sWx _ rw) => rs.
move:(cover_at_pr fpa us rw) => pa.
hnf; rewrite  isc_rel_sr //; split=> //.
set_extens t.
  move => ts.
  have tx: inc t x by rewrite - (proj33 fpa); union_tac.
  apply /(class_P ec) /isc_rel_P /(isc_rel1P rs tx).
  by symmetry; apply:(same_cover_at fpa rs);rewrite pa.
move /(class_P ec) /isc_rel_P => h; move: (proj2 (isc_hi h)) => tx.
rewrite -pa; move: (proj1 (cover_at_in fpa tx)).
by move /(isc_rel1P rs tx): h => ->.
Qed.

Lemma partition_fun_fb:
  (allf (graph f) nonempty) ->
  bijection (Lf (Vf f)  (source f) (quotient (partition_relation f x))).
Proof. 
move: isc_rel_equivalence => er.
rewrite /allf - (proj33 ff); move=> alne; apply: lf_bijective.
- move=> t tf; apply/(setQ_P er). 
  apply: isc_rel_class2 =>//; apply: (alne _ tf). 
- move=> u v us vs sW.
  move: (alne _ us)=> [y yu]; have yv: (inc y (Vf f v)) by rewrite - sW.
  by apply: (partition_inc_unique1 us yu vs yv).
- move=> y; move/(setQ_P er) => ic.
  move: (isc_rel_class ic) => [u us] ->; ex_tac.
Qed.

End InSameCoset.

(** A system of representatives for the partition f of x as a set f 
   or a function g *)

Definition representative_system s f x :=
  [/\ function f, partition_w_fam (graph f) x, sub s x 
  & forall i, inc i (source f) -> singletonp ((Vf f i) \cap s)].

Definition representative_system_function g f x :=
  injection g /\ (representative_system (range (graph g)) f x).

Lemma rep_sys_function_pr g f x i:
  representative_system_function g f x -> inc i (source f) ->
  exists! a, (inc a (source g) /\ inc (Vf g a) (Vf f i)).
Proof. 
move=> [[fg ig] [ff pf gg  alsi]] ins.
move: (alsi _ ins) => [u isu].
apply /unique_existence; split.
  move: (set1_1 u). 
  rewrite - isu; move /setI2_P => [pa] /(range_fP fg) [a asg pb]. 
  by exists a; rewrite - pb.
move=> a b [asg Wa][bsg Wb]; apply: ig => //.
have aux: (forall a, inc a (source g) -> inc (Vf g a) (Vf f i) -> Vf g a = u).
  move=> c csg Wc.
  apply: set1_eq; rewrite -isu; apply: setI2_i => //; Wtac.
rewrite aux // aux //.
Qed.

Lemma rep_sys_function_pr2 g f x:
  injection g -> function f -> partition_w_fam (graph f) x ->
  sub (target g) x  ->
  (forall i, inc i (source f) ->
      exists! a, (inc a (source g) /\ inc (Vf g a) (Vf f i))) ->
  representative_system_function g f x.
Proof.
move=> ig ff pf stx exu; move:(ig)=> [fg _].
split =>//; split=>//.
  by apply: (@sub_trans (target g)); [apply: f_range_graph |].
move=> i isf; move: (exu _ isf) => [a [[asg Wa] un]].
exists (Vf g a); set_extens t.
  move/setI2_P => [tv /(range_fP fg) [z zsg eq]]; apply/set1_P. 
  by rewrite eq;congr (Vf g _); symmetry;apply: un;rewrite - eq.
move /set1_P => ->; apply/setI2_P; split => //; Wtac.
Qed.

Lemma section_canon_proj_pr g f x y r:
  r = partition_relation f x ->  function f -> partition_w_fam (graph f) x ->
  is_right_inverse (canon_proj r) g ->
  inc y x ->
  related r y (Vf g (class r y)).
Proof. 
move=> pr ff pf ri yx.
have eq: equivalence r by rewrite pr; apply: isc_rel_equivalence.
have sr: substrate r = x by rewrite pr isc_rel_sr //. 
rewrite - sr in yx.
have cyq: inc (class r y) (quotient r) by fprops.
have sg: source g = target (canon_proj r) by apply: right_i_source.
move: sg; aw => sg; rewrite - sg in cyq.
have yri: inc y (class r y) by apply: inc_itself_class => //.
apply: (symmetricity_e eq).
apply /(class_P eq).
have <- //: (class r y) = class r (Vf g (class r y)).
have [pa pb] := ri.
set t := (class r y).
have Wcs: inc (Vf g t) (substrate r) by move: pa=> [_ fg]; aw; move=>->; Wtac.
have: Vf (canon_proj r \co g) t = Vf  (canon_proj r) (Vf g t) by aw.  
rewrite pb; bw; aw; rewrite /t;fprops.
Qed.

Lemma section_is_representative_system_function g f x:
  function f -> partition_w_fam (graph f) x ->
  is_right_inverse  (canon_proj (partition_relation f x)) g ->
  (forall u, inc u (source f) -> nonempty (Vf f u)) ->
  representative_system_function g f x.
Proof. 
move=> ff pf ti alne.
have ig: injection g by apply: (right_inverse_fi ti). 
apply: rep_sys_function_pr2=>//.  
  rewrite - (proj33 (proj1 ti)) canon_proj_s isc_rel_sr; fprops.
move=> i isf.
set (r:=partition_relation f x) in *.
have sf: domain (graph f) =source f by apply: f_domain_graph. 
have er: equivalence r by rewrite /r; apply: isc_rel_equivalence.
have sr: substrate r = x by rewrite /r isc_rel_sr.
rewrite (right_i_source ti); aw.
apply /unique_existence;split.
  set z:= (rep (Vf f i)).
  have zW: inc z (Vf f i) by rewrite /z; apply: rep_i; apply: alne.
  have zx: inc z x by move: pf=>[_ md <-];  rewrite - sf in isf; union_tac. 
  exists (class r z); split. 
    aw; rewrite - sr in zx; fprops. 
  move: (section_canon_proj_pr (refl_equal r) ff pf ti zx).
  move /(isc_rel_P ff pf) => [ u [usf zW' qW]]. 
  by rewrite (partition_inc_unique1 ff pf isf zW usf zW'). 
aw; move=> a b [atx Wa] [btx Wb].
have Wiq: inc (Vf f i) (quotient r).
  apply/(setQ_P er); apply (isc_rel_class2 ff pf isf); ex_tac.
have aux: (forall u, inc u (quotient r) -> inc (Vf g u) (Vf f i) -> Vf f i = u).
  move=> u /(setQ_P er) [rs eq] iWW; rewrite sr in rs.
  rewrite eq; apply: is_class_pr=> //.
  move: (section_canon_proj_pr (refl_equal r) ff pf ti rs).
  rewrite - eq; move /(isc_rel_P ff pf) => [v [usf zW' qW]].
  by rewrite (partition_inc_unique1 ff pf isf iWW usf qW). 
by rewrite -(aux _ atx Wa) (aux _ btx Wb).
Qed.


(** ** EII-6-3 Relations compatible with an equivalence relation *)

(** A relation is compoatible if the set of objects satisfying the relation is a union of classes *)

Definition compatible_with_equiv_p (p: property) (r:Set) :=
  forall x x', p x -> related r x x' -> p x'.

Lemma trivial_equiv p x:
  compatible_with_equiv_p p (diagonal x).
Proof. by move=> u v pa /diagonal_pi_P [_] <-. Qed.

(** A compatible relation induces a relation on the quotient *)

Definition relation_on_quotient p r :=
  fun t => inc t (quotient r) /\ exists2 x, inc x t & p x.

Lemma rel_on_quoP p r:
  equivalence r -> compatible_with_equiv_p p r -> forall t,
  (relation_on_quotient p r t <-> 
     (inc t (quotient r) /\  forall x, inc x t -> p x)).
Proof. 
move=> er co t; split.
  move=> [tq [x xt px]]; split=>// u ut; apply: (co _  _ px).  
  by move: tq => /(setQ_P er) h; apply /(in_class_relatedP er); exists t.
move => [tq xtpx];move: (setQ_ne er tq) => /rep_i net.
split =>//; ex_tac.
Qed.

Lemma rel_on_quoP2 p r:
  equivalence r -> compatible_with_equiv_p p r -> forall y,
  ( (inc y (substrate r) /\ relation_on_quotient p r (Vf (canon_proj r) y)) <->
    (inc y (substrate r) /\ p y)).
Proof.
move=> er co; split; move => [ysr]; rewrite (canon_proj_V ysr).
  move => [tq [x xt px]]. 
  have yx: related r x y by move : xt; move /(class_P er) => h; equiv_tac. 
  by split =>//; apply: (co _ _  px yx).
move => py;split =>//; split; fprops.
move:(inc_itself_class er ysr) => h; ex_tac.
Qed.

(** ** EII-6-4 saturated subsets *)

(** A set is satured if it is a union of classes*)

Definition saturated r x  := compatible_with_equiv_p (fun y=> inc y x) r.


(** If f is the canonical projection this defines that smallest saturated set that contains x*)

Definition inverse_direct_value f x :=
  Vfs (inverse_fun f) (Vfs f x).

Lemma idvalue_P f x: function f -> sub x (source f) ->forall y,
  inc y (inverse_direct_value f x) <-> 
    (inc y (source f) /\  (exists2 z, inc z x & Vf f y = Vf f z)).
Proof.
move => ff sxf.
split.
  move /dirim_P => [u]; aw; move /dirim_P => [z zx pa] /igraph_pP pb.
  split; [Wtac | by ex_tac; rewrite - (Vf_pr ff pa) - (Vf_pr ff pb) ].
move => [ysf [z zx  pa]].
apply/dirim_P; exists (Vf f z).
   apply/dirim_P;ex_tac; Wtac.  
aw; apply/igraph_pP; rewrite -pa; Wtac.
Qed.

Lemma idvalue_cprojP r x: 
  equivalence r -> sub x (substrate r) ->forall y,
  inc y (inverse_direct_value (canon_proj r) x) <-> 
    (inc y (substrate r) /\ (exists2 z, inc z x & class r y = class r z)).
Proof.
have ff:= (canon_proj_f r).
move => pa pb; move: (pb); rewrite - canon_proj_s => pc y.
split.
  move/(idvalue_P ff pc) => [qa [v qb vx]]; split; first by exact.
  have ysr: inc y (substrate r) by rewrite - canon_proj_s.
  by ex_tac; move: vx; aw ;apply: pb.
move => [qa [v qb qc]]; apply/(idvalue_P ff pc).
have vsr: inc v (substrate r) by apply: pb.
have ysr: inc y (substrate r) by move: qa; aw.
split => //;exists v; aw.
Qed.

Lemma saturatedP r x:
  equivalence r -> sub x (substrate r) ->
  ((saturated r x) <-> (forall y, inc y x -> sub (class r y) x)).
Proof. 
move=> er sxs; split.
  move=> sr y yx t; move/(class_P er); apply: (sr _ _  yx). 
by move=> yw u v ux ruv; apply: (yw _ ux); apply/(class_P er).
Qed.

Lemma saturated2P r x:
  equivalence r -> sub x (substrate r) ->
  ((saturated r x) <->
      exists2 y, (forall z, inc z y -> classp r z) & x = union y).
Proof. 
move => er sxs; move: (saturatedP er sxs) => aux;split.
  move => srx.
  exists (Zo (powerset x)(fun z => exists2 a, inc a x & z = class r a)).
    move=> z /Zo_P [] /setP_P zx [a ax ->]. 
    by apply: class_class =>//; apply: sxs.
  set_extens t => ts. 
    apply: (@setU_i _ (class r t)). 
      by move: (sxs _ ts)=>h; apply/(class_P er);equiv_tac.
    apply: Zo_i; [ by apply/setP_P;move /aux: srx; apply | ex_tac].
  by move /setU_P: ts => [y ty /Zo_P [] /setP_P yx [a ax yc]]; apply: yx.
move => [y yp xu]; apply/aux; rewrite xu => z zu.
move: (setU_hi zu) =>[t zt ty]; move: (yp _ ty) => ct.
move => u /(class_P er) rz; apply:(setU_i _ ty).
have pa := (rel_in_class er ct zt).
rewrite (proj2 (yp _ ty)); apply /(class_P er); equiv_tac. 
Qed.


Lemma class_is_inv_direct_value r x:
  equivalence r -> inc x (substrate r) ->
  class r x = inverse_direct_value (canon_proj r) (singleton x).
Proof.
move=> er xs.
move: (set1_sub xs) => xs1.
set_extens t => ts.
  apply/(idvalue_cprojP er xs1); split.
    exact: (sub_class_substrate er ts).
  exists x; fprops; exact :(class_eq2 er ts).
move/(idvalue_cprojP er xs1): ts => [v [pa /set1_P <- <-]]; fprops.
Qed.

Lemma saturated_P3 r x:
  equivalence r -> sub x (substrate r) ->
  (saturated r x <-> (x= inverse_direct_value (canon_proj r) x)).
Proof. 
move=> er xs.
set (p:=canon_proj r). 
have fp: function p by rewrite /p; fprops.
split => h.
  apply: extensionality.  
    by apply: inverse_direct_image =>//; rewrite /p; aw.
  move => y /(idvalue_cprojP er xs) [z [pa pb pc]].
  move /(saturatedP er xs): h => q; move: (q _ pb); rewrite -pc.
  apply; fprops.
apply/(saturatedP er xs); rewrite {2} h => y yx t tc.
apply /(idvalue_cprojP er xs); split.
  exact: (sub_class_substrate  er tc).
ex_tac;exact:(class_eq2 er tc).
Qed.

Lemma saturated_P4 r x:
  equivalence r -> sub x (substrate r) ->
  (saturated r x <-> (exists2 b, sub b (quotient r) 
    & x = Vfs (inverse_fun (canon_proj r)) b)).
Proof.
move=> er xs.
have qr: quotient r = target (canon_proj r) by aw.
have sj := (canon_proj_fs er).
split. 
  move/(saturated_P3 er xs) => hyp. 
  exists (Vfs (canon_proj r) x) =>//.
  rewrite qr;apply: sub_trans (f_range_graph (proj1 sj)); apply: dirim_Sr. 
move=> [b bq xeq].
apply/(saturated_P3 er xs).
rewrite qr in bq; move: (direct_inv_im_surjective sj bq).
by rewrite /inverse_direct_value -xeq => ->.
Qed.

(** Links between saturation and union, intersection, complement *)

Lemma saturated_setU r x:
  equivalence r ->
  (alls x (sub^~ (substrate r))) -> (alls x (saturated r)) ->
  (sub (union x) (substrate r) /\  saturated r (union x)).
Proof. 
move=> er als alsa.
have r1: (sub (union x) (substrate r)).
  by move => t /setU_P [z tz zx]; apply: (als _ zx).
split=>//;apply /saturatedP => // y /setU_P [z yz zx]. 
apply: sub_trans (setU_s1 zx).
by move: (alsa _ zx)  => /(saturatedP er (als _ zx)); apply.
Qed.

Lemma saturated_setI r x:
  equivalence r -> nonempty x ->
  (alls x (sub^~ (substrate r))) -> (alls x (saturated r)) ->
  (sub (intersection x) (substrate r) /\  saturated r (intersection x)).
Proof. 
move=> er nex als alsa.
have aux: (sub (intersection x) (substrate r)). 
  by move: nex => [y yx]; apply: sub_trans (als _ yx); apply: setI_s1.
split =>//; apply /(saturatedP er aux) => y yi t tc; apply: (setI_i nex). 
move=> z zx; move:(alsa _ zx). 
move /(saturatedP er (als _ zx))=> s; apply: (s _ (setI_hi yi zx) _ tc). 
Qed.

Lemma saturated_setC r a:
  equivalence r -> sub a (substrate r) -> saturated r a -> 
  saturated r ((substrate r) -s a).
Proof. 
move=> er ar.
move /(saturated_P4 er ar) => [b sq aib].
apply /(saturated_P4 er);first by apply: sub_setC.
exists ((quotient r) -s b); first by apply: sub_setC.
move: (iim_fun_C b (canon_proj_f r)). 
by rewrite aib iim_fun_pr canon_proj_s canon_proj_t. 
Qed.

Definition saturation_of r x :=
  inverse_direct_value (canon_proj r) x.

Lemma saturation_of_pr r x:
  equivalence r -> sub x (substrate r) ->
  saturation_of r x =
  union (Zo (quotient r)(fun z=> exists2 i, inc i x & z = class r i)).
Proof. 
move=> er sr.
have fc: function (canon_proj r) by fprops.
rewrite /saturation_of/inverse_direct_value. 
set_extens y.
  move /(idvalue_cprojP er sr) => [v [pa pb pc]].
  apply: (@setU_i  _ (class r y)); fprops; apply: Zo_i; fprops.
  by ex_tac; rewrite pd.
move /setU_P => [z zy/Zo_P [zq [i ix sc]]].
move: zy; rewrite sc; move/(class_P er) => pc.
apply/(idvalue_cprojP er sr); split;first by substr_tac.
ex_tac;symmetry;by apply:class_eq1.
Qed.


Lemma saturation_of_smallest r x:
  equivalence r -> sub x (substrate r) ->
  [/\ saturated r (saturation_of r x),
    sub x (saturation_of r x) 
    & (forall y, sub y (substrate r) -> saturated r y -> sub x y
      -> sub (saturation_of r x) y)].
Proof.
move=> er xsr.
have fc: function (canon_proj r) by fprops.
split.
- apply /(saturated_P4 er). 
    by move => t /(idvalue_cprojP er xsr) [pa _].
  exists (Vfs (canon_proj r) x) => //.
  rewrite - canon_proj_t.
  apply: sub_trans (f_range_graph fc); apply: dirim_Sr.
- move => t tx; apply/(idvalue_cprojP er xsr); split; [by apply: xsr| ex_tac].
- move=> y ys sy sxy t.
  move /(idvalue_cprojP er xsr) => [tsr [z tx sc]].
  move /(saturated_P3 er ys): sy => ->.
  by apply/(idvalue_cprojP er ys); split => //; exists z => //; apply: sxy.
Qed.

Definition union_image x f:=
  union (Zo x (fun z=> exists2 i, inc i (source f) & z = Vf f i)).

Lemma saturation_of_union r f g:
  equivalence r -> function f -> function g ->
  (forall i, inc i (source f) -> sub (Vf f i) (substrate r)) ->
  source f = source g ->
  (forall i, inc i (source f) -> saturation_of r (Vf f i) = Vf g i)
  -> saturation_of r (union_image (powerset(substrate r)) f) = 
  union_image (powerset(substrate r)) g.
Proof.
move=> er ff fg als sfsg alsat.
have fc: function (canon_proj r) by fprops.
have U1sr: sub (union_image (powerset (substrate r)) f) (substrate r).
  by move => t /setU_P [z zt /Zo_P [/setP_P h _]]; apply: h.
set_extens x. 
  move/(idvalue_cprojP er U1sr) => [zu [z /setU_P [v zv]] /Zo_P []
     /setP_P vsr [i isf fi] sc].
  move:(als _ isf) => pa.
  apply/setU_P; exists (Vf g i); rewrite -(alsat _ isf).
    apply/(idvalue_cprojP er pa); split => //; exists z => //; ue.
  apply: Zo_i; first by apply/setP_P=> t /(idvalue_cprojP er pa) [ ok _].
  rewrite - sfsg; ex_tac.
move => /setU_P [z xz /Zo_P [/setP_P zr [i isr zv]]].
move: xz; rewrite - sfsg in isr; rewrite zv - (alsat _ isr).
move/(idvalue_cprojP er (als _ isr)) => [pa [t pb pc]].
apply/(idvalue_cprojP er U1sr); split => //; exists t => //.
apply /setU_P; exists (Vf f i) => //; apply:Zo_i; last by ex_tac.
by apply /setP_P; apply: als.
Qed.

(** ** EII-6-5 Mappings compatible with equivalence relations *)

(** The canonical projection is surjective, thus has a section *)

Definition section_canon_proj r :=
  Lf rep (quotient r) (substrate r).

Lemma section_canon_proj_axioms r:
  equivalence r ->
  lf_axiom rep (quotient r) (substrate r).
Proof. move=> er t ta; fprops. Qed.

Lemma section_canon_proj_V r x:
  equivalence r ->
  inc x (quotient r) -> Vf (section_canon_proj r) x = (rep x).
Proof.
rewrite/section_canon_proj=> er iq; aw.  
by apply: section_canon_proj_axioms. 
Qed.

Lemma section_canon_proj_f r:
  equivalence r -> function (section_canon_proj r).
Proof. 
rewrite/section_canon_proj=> er. 
by apply: lf_function; apply: section_canon_proj_axioms.
Qed.

Lemma right_inv_canon_proj r:
  equivalence r ->
  is_right_inverse (canon_proj r) (section_canon_proj r).
Proof. 
move=> er.
have ss: source (section_canon_proj r) = quotient r.
  by rewrite/section_canon_proj; aw.
have fs: function (section_canon_proj r) by apply: section_canon_proj_f.
have fc: function (canon_proj r) by fprops.
have cpo: (canon_proj r) \coP (section_canon_proj r).
  split => //; rewrite/ section_canon_proj; aw.
split=> //. 
apply: function_exten; try fct_tac; fprops; aw.
rewrite ss=> x xs.  
have aux: (Vf (section_canon_proj r) x) = rep x.
  by rewrite section_canon_proj_V //.  
aw; try ue. 
rewrite identity_V // aux; apply: class_rep =>//.
Qed.

(** A mapping is compatible with an equivalence if it is constant on classes; 
   it is compatible with two equivalences is the image of a class is a 
   subset of a class *)

Definition compatible_with_equiv f r :=
  [/\ function f, source f = substrate r &
  forall x x', related r x x' -> Vf f x = Vf f x'].

Definition compatible_with_equivs f r r' :=
  [/\ function f, target f =  substrate r' &
  compatible_with_equiv ((canon_proj r') \co f) r].

(* This is the definition of Bourbaki *)

Lemma compatible_with_equiv_pr f r:
  function f -> source f = substrate r  ->
  (compatible_with_equiv f r <->
    (forall y, compatible_with_equiv_p (fun x => y = Vf f x) r)).
Proof. 
move=> ff sf; rewrite/compatible_with_equiv/compatible_with_equiv_p. 
split.
  by move=> [_ _ hyp] y x x' => ->; apply: hyp.
by move=> hyp; split => // x x'; apply: (hyp (Vf f x) x x'). 
Qed.

Lemma compatible_constant_on_classes f r x y:
  equivalence r ->
  compatible_with_equiv f r -> inc y (class r x) -> Vf f x = Vf f y.
Proof. 
by move=> eq [ff sf hyp] yc; apply: hyp; move/(class_P eq): yc.
Qed.

Lemma compatible_constant_on_classes2 f r x:
  equivalence r -> compatible_with_equiv f r -> 
  constantfp (restriction f (class r x)).
Proof.
move=> re [ff sf hyp].
have scs: sub (class r x) (substrate r) by apply: sub_class_substrate.
rewrite - sf in scs.
split; first by apply: (proj31 (restriction_prop ff scs)).
have sr: source (restriction f (class r x)) = class r x.
  by rewrite /restriction; aw.
rewrite sr.  
move=> a b ac bc /=; rewrite ! restriction_V //; apply: hyp.
move: ac bc => /(class_P re) ac /(class_P re) bc; equiv_tac.
Qed.

Lemma compatible_with_proj f r x y:
  equivalence r -> compatible_with_equiv f r -> 
  inc x (substrate r) -> inc y (substrate r) -> 
  Vf (canon_proj r) x = Vf (canon_proj r) y -> Vf f x = Vf f y.
Proof. 
move=> er cgt xs ys; aw => sx.
apply: (@compatible_constant_on_classes _ r) =>//; rewrite sx; fprops.
Qed.

Lemma compatible_with_pr r r' f x y:
  equivalence r ->  equivalence r' ->
  compatible_with_equivs f r r' -> 
  related r x y -> related r' (Vf f x) (Vf f y).
Proof. 
move=> er er'  [ff sf [fc sc hyp]] rxy.
have cc: ((canon_proj r') \coP f) by split; first (by fprops); aw.
move: sc; aw => sc.
have xs: inc x (source f) by rewrite sc; substr_tac.
have ys: inc y (source f) by rewrite sc; substr_tac.
have px: (inc (Vf f x) (substrate r')) by Wtac.
have py: (inc (Vf f y) (substrate r')) by Wtac.
move: (hyp _ _ rxy); aw =>// sc1.
by apply/related_equiv_P.
Qed.

Lemma compatible_with_pr2 r r' f:
  equivalence r ->  equivalence r' ->
  function f ->
  target f = substrate r'-> source f = substrate r->
  (forall x y,  related r x y -> related r' (Vf f x) (Vf f y)) ->
  compatible_with_equivs f r r'.
Proof.
move=> er er' ff tf sf rr'.
have cc: (canon_proj r') \coP f by split; fprops; symmetry; aw.
split =>//; split=>//; aw;first by fct_tac.
move=> x x' rxx'; move: (rr' _ _ rxx'); move /(related_equiv_P er').
move => [Ws Ws' cxx']; aw; rewrite sf; substr_tac.  
Qed.

Lemma compatible_with_proj3  r r' f x y:
  equivalence r -> equivalence r' -> 
  compatible_with_equivs f r r'->
  inc x (substrate r) -> inc y (substrate r) ->
  Vf (canon_proj r) x = Vf (canon_proj r) y -> 
  class r' (Vf f x) = class r' (Vf f y).
Proof.
move=> er er' co xs ys; aw => sc.
apply: class_eq1 =>//; apply: (compatible_with_pr er er' co).
by apply /(related_equiv_P er). 
Qed. 

(** A compatible mapping induces a mapping on the quotient *)

Definition fun_on_quotient r f :=
  f \co (section_canon_proj r).

Lemma exists_fun_on_quotient f r:
  equivalence r -> function f -> source f = substrate r ->
  (compatible_with_equiv f r <->
  (exists h, h \coP (canon_proj r) /\ h \co (canon_proj r) = f)).
Proof.
move=> er ff sf.
rewrite exists_left_composable; aw; try apply: canon_proj_fs=>//.
split. 
  by move => co x y xs ys sW; apply: (compatible_with_proj er co xs ys sW). 
move=> hyp; split=>//.
move=> x x' /(related_equiv_P er)  [xs ys cc];apply: hyp; aw.
Qed.

Lemma exists_unique_fun_on_quotient f r h:
  equivalence r -> compatible_with_equiv f r ->
  h \coP (canon_proj r) -> h \co (canon_proj r) = f ->
  h = fun_on_quotient r f.
Proof. 
move=> er cfr chc chcf; move: (cfr) => [ff sf1 _].
have sc: (surjection (canon_proj r)) by apply: canon_proj_fs.
have ri := (right_inv_canon_proj er).
have sf: source f = source (canon_proj r) by aw.
apply: (exists_left_composable_aux ff sf ri chc chcf).
Qed.

Lemma compose_foq_proj f r:
  equivalence r ->  compatible_with_equiv f r ->
  (fun_on_quotient r f) \co (canon_proj r) = f.
Proof.
move=> er co; move: (co)=> [ff sf hyp].
set (g:= canon_proj r). 
have sg: surjection g by rewrite/g; apply: canon_proj_fs.
have sfsg: source f = source g by rewrite /g; aw.
have sW: forall x y, inc x (source g) ->  inc y (source g) ->
     Vf g x = Vf g y -> Vf f x = Vf f y. 
  rewrite - sfsg sf; move=> x y xr yr h.
  by apply: (compatible_with_proj er co xr yr). 
apply: (left_composable_value ff sg sfsg sW (right_inv_canon_proj er) 
    (refl_equal (fun_on_quotient r f))).
Qed.

(** A mapping compatible with two relations induces a mapping on the two quotients *)

Definition fun_on_rep f: Set -> Set := fun x=> f(rep x).
Definition fun_on_reps r' f := fun x=> Vf (canon_proj r') (f(rep x)) .

Definition function_on_quotient r f b  :=
  Lf (fun_on_rep f)(quotient r)(b).

Definition function_on_quotients r r' f :=
  Lf (fun_on_reps r' f)(quotient r)(quotient r').

Definition fun_on_quotients r r' f :=
  ((canon_proj r') \co f) \co (section_canon_proj r).

Lemma foq_axioms r f b:
  equivalence r ->
  lf_axiom f (substrate r) b ->
  lf_axiom (fun_on_rep f) (quotient r) b.
Proof. move=> er h x xs;apply: h; fprops. Qed.

Lemma foqs_axioms r r' f:
  equivalence r ->
  equivalence r' ->
  lf_axiom f (substrate r)(substrate r') ->
  lf_axiom (fun_on_reps r' f) (quotient r) (quotient r').
Proof.
move => er er' h x xs. 
have w: (inc (rep x) (substrate r)) by fprops. 
rewrite /fun_on_reps; aw; fprops.
Qed.

Lemma foqc_axioms r f:
  equivalence r ->
  function f -> source f = substrate r ->
  f \coP (section_canon_proj r).
Proof. 
move=> er ff sf. 
split =>//; first by apply: section_canon_proj_f. 
rewrite /section_canon_proj; aw. 
Qed.

Lemma foqcs_axioms r r' f:
  equivalence r ->
  equivalence r' ->
  function f -> source f = substrate r -> target f = substrate r' ->
  (canon_proj r' \co f) \coP (section_canon_proj r).
Proof. 
move=> er er' ff sf tf.
have fc: (function (canon_proj r')) by fprops. 
split; first by fct_tac => //; symmetry; aw.
  by apply: section_canon_proj_f. 
rewrite/section_canon_proj; aw.
Qed.

Lemma foq_f r f b:
  equivalence r ->
  lf_axiom f (substrate r) b ->
  function (function_on_quotient r f b).
Proof. 
by rewrite /function_on_quotient=> *; apply: lf_function; apply: foq_axioms.
Qed.

Lemma foqs_f r r' f:
  equivalence r ->
  equivalence r' ->
  lf_axiom f (substrate r)(substrate r') ->
  function (function_on_quotients r r' f).
Proof.
by rewrite /function_on_quotients=> *;apply: lf_function; apply: foqs_axioms.
Qed.

Lemma foqc_f r f:
  equivalence r -> function f ->
  source f = substrate r ->
  function (fun_on_quotient r f).
Proof. 
rewrite/fun_on_quotient=> er ff sf; fct_tac. 
  by apply: section_canon_proj_f.
by rewrite /section_canon_proj; aw.
Qed.

Lemma foqcs_f r r' f:
  equivalence r ->
  equivalence r' ->
  function f -> source f = substrate r -> target f = substrate r' ->
  function (fun_on_quotients r r' f).
Proof. 
rewrite/fun_on_quotients=> er er' ff sf tf.
by apply: compf_f; apply: foqcs_axioms.
Qed.

Lemma foq_V r f b x:
  equivalence r ->
  lf_axiom f (substrate r) b ->
  inc x (quotient r) ->
  Vf (function_on_quotient r f b) x = f (rep x).
Proof. 
by rewrite /function_on_quotient=> er ta xq; aw; apply: foq_axioms. 
Qed.

Lemma foqc_V r f x:
  equivalence r -> function f ->
  source f = substrate r -> inc x (quotient r) ->
  Vf (fun_on_quotient r f) x = Vf f (rep x).
Proof. 
rewrite/fun_on_quotient=>  er ff sf xq; aw.     
    by rewrite section_canon_proj_V. 
  by apply: foqc_axioms.
by rewrite /section_canon_proj; aw.
Qed.

Lemma foqs_V r r' f x:
  equivalence r ->
  equivalence r' ->
  lf_axiom f (substrate r)(substrate r') ->
  inc x (quotient r) ->
  Vf (function_on_quotients r r' f) x = class r' (f (rep x)).
Proof.
rewrite /function_on_quotients=> er er' ta xq; aw. 
  by rewrite /fun_on_reps; aw; apply: ta; fprops. 
by apply: foqs_axioms.
Qed.

Lemma foqcs_V r r' f x:
  equivalence r ->
  equivalence r' ->
  function f -> source f = substrate r -> target f = substrate r' ->
  inc x (quotient r) ->
  Vf (fun_on_quotients r r' f) x = class r' (Vf f (rep x)).
Proof. 
move=> er er' ff sf tf xq.
rewrite /fun_on_quotients. 
have fs: function(section_canon_proj r) by apply: section_canon_proj_f.
have ccf: (canon_proj r') \coP f by split; fprops; symmetry;aw.
have cc2: ( (canon_proj r') \co f) \coP (section_canon_proj r).
  by split; first (by fct_tac); rewrite /section_canon_proj; aw.
have Wt: inc (Vf (section_canon_proj r) x) (target (section_canon_proj r)).
  by Wtac; rewrite /section_canon_proj; aw.
have irs: inc (rep x) (source f) by ue.
rewrite compf_V //; last by  rewrite/section_canon_proj; aw.
rewrite section_canon_proj_V // /section_canon_proj.
aw; Wtac. 
Qed.

Lemma fun_on_quotient_pr r f x:
  Vf f x = fun_on_rep (fun _ => Vf f x) (Vf (canon_proj r)x).
Proof. done. Qed.

Lemma fun_on_quotient_pr2 r r' f x:
  Vf (canon_proj r')  (Vf f x) = 
  fun_on_reps r' (fun _ => Vf f x) (Vf (canon_proj r) x).
Proof. trivial. Qed.

Lemma composable_fun_proj r f b:
  equivalence r -> 
  lf_axiom f (substrate r) b ->
  (function_on_quotient r f b) \coP (canon_proj r).
Proof. 
move=> er ta. 
split; [by apply: foq_f | fprops | rewrite/function_on_quotient; aw ].
Qed.

Lemma composable_fun_projs r r' f:
  equivalence r -> 
  equivalence r' -> 
  lf_axiom f (substrate r) (substrate r') ->
  (function_on_quotients r r' f) \coP (canon_proj r).
Proof.
move=> er er' ta.
split; [by apply: foqs_f | fprops | rewrite/function_on_quotients; aw ].
Qed.

Lemma composable_fun_projc r f:
  equivalence r -> 
  compatible_with_equiv f r ->
  (fun_on_quotient r f) \coP (canon_proj r).
Proof. 
move=> er [ff sf h].
split; [ by apply: foqc_f | fprops | ].
rewrite/fun_on_quotient/section_canon_proj; aw.
Qed.

Lemma composable_fun_projcs r r' f:
  equivalence r -> equivalence r' -> 
  compatible_with_equivs f r r'->
  (fun_on_quotients r r' f) \coP (canon_proj r).
Proof. 
move=> er er'  [ff sf [fg sg h]].
move: sg; aw => sg.
split; fprops;first by apply: foqcs_f.  
rewrite/fun_on_quotients/section_canon_proj; aw.
Qed.


Lemma fun_on_quotient_pr3 r f x:
  equivalence r -> inc x (substrate r) ->  
  compatible_with_equiv f r ->
  Vf f x = Vf (fun_on_quotient r f) (Vf  (canon_proj r) x).
Proof. 
move=> er xs co; rewrite - compf_V; last by aw.
  by rewrite compose_foq_proj. 
by apply: composable_fun_projc.
Qed.


(** Figure 3 (French version only) *)

Lemma fun_on_quotient_pr4 r r' f:
  equivalence r -> equivalence r' -> 
  compatible_with_equivs f r r'->
  (canon_proj r') \co f = (fun_on_quotients r r' f) \co (canon_proj r).
Proof. 
rewrite/fun_on_quotients; move=> er er' [ff sf h].
symmetry; apply: (compose_foq_proj er h).
Qed.

Lemma fun_on_quotient_pr5 r r' f x:
  equivalence r -> equivalence r' -> 
  compatible_with_equivs f r r'->
  inc x (substrate r) ->  
  Vf (canon_proj r') (Vf f x)  =
  Vf (fun_on_quotients r r' f) (Vf (canon_proj r) x). 
Proof. 
move => er er' co  xs.
move: (co)=> [ff sf [fg sg h]]; move: sg; rewrite compf_s => sg.
have cc: composable (canon_proj r') f by split; fprops;symmetry; aw.
rewrite - compf_V //; try ue. 
rewrite - compf_V //; last by aw.
  by rewrite -fun_on_quotient_pr4 //.
by apply: composable_fun_projcs=>//.
Qed.

Lemma compose_fun_proj_ev r f b x:
  equivalence r -> 
  compatible_with_equiv (Lf f (substrate r) b) r -> 
  inc x (substrate r) ->
  lf_axiom f (substrate r) b ->
  Vf (function_on_quotient r f b \co canon_proj r) x = f x.
Proof. 
move=> er co xr ta.
have cq: (inc (class r x) (quotient r)) by fprops.
aw; try apply: composable_fun_proj =>//; last by aw.
have rrx: related r (rep (class r x)) x.
  by apply: symmetricity_e=>//; apply: related_rep_class=>//.
rewrite foq_V //; move: (proj33 co _ _ rrx); aw; fprops.
Qed.

Lemma compose_fun_proj_ev2 r r' f x:
  equivalence r -> 
  equivalence r' -> 
  compatible_with_equivs (Lf f (substrate r) (substrate r')) r r' -> 
  lf_axiom f (substrate r) (substrate r') ->
  inc x (substrate r) ->
  inc (f x) (substrate r') ->
  Vf (canon_proj r') (f x)  =
  Vf (function_on_quotients r r' f \co canon_proj r) x.
Proof. 
move=> er er' co ta xs fxs. 
aw; try apply: composable_fun_projs =>//; last by aw.
set (y:= (Vf (canon_proj r) x)). 
have : (Vf (function_on_quotients r r' f) y
    = (Vf (fun_on_quotients r r' (Lf f (substrate r) (substrate r'))))y). 
  have ys: inc y (quotient r) by rewrite /y; aw; fprops.
  have h :=(rep_i_sr er ys).
  by rewrite foqs_V // foqcs_V //; aw; apply: lf_function.
by rewrite - fun_on_quotient_pr5 // /y; aw => ->.
Qed.

Lemma compose_fun_proj_eq r f b:
  equivalence r -> 
  compatible_with_equiv (Lf f (substrate r) b) r -> 
  lf_axiom f (substrate r) b ->
  (function_on_quotient r f b) \co (canon_proj r) = 
    Lf f (substrate r) b.
Proof.
move=> er co ta.
apply: function_exten; try solve [ rewrite/function_on_quotient; aw].
- apply: compf_f; apply: composable_fun_proj=>//. 
- apply: lf_function =>//.  
- rewrite /function_on_quotient; aw. 
  by move =>x xs /=; rewrite compose_fun_proj_ev=>//; aw.
Qed.

Lemma compose_fun_proj_eq2 r r' f:
  equivalence r -> 
  equivalence r' -> 
  lf_axiom f (substrate r) (substrate r') ->
  compatible_with_equivs (Lf f (substrate r) (substrate r')) r r'->
  (function_on_quotients r r' f) \co (canon_proj r) = 
  (canon_proj r') \co (Lf f (substrate r) (substrate r')).
Proof.
move=> er er' ta co.
have ffoq:function (function_on_quotients r r' f) by apply: foqs_f.
have fa: function  (Lf f (substrate r) (substrate r')) by apply: lf_function.
have cn: (function_on_quotients r r' f) \coP (canon_proj r).
  by split; fprops; rewrite/function_on_quotients; aw.  
have cc: (canon_proj r') \coP (Lf f (substrate r) (substrate r')).
  by split; fprops; aw.
apply: function_exten; try fct_tac; aw.  
  rewrite /function_on_quotients; aw. 
move => x xs.
have aux: (inc (f x) (substrate r')) by apply: ta.
rewrite -compose_fun_proj_ev2 //; aw. 
Qed.

Lemma compatible_ea f:
  function f ->
  compatible_with_equiv f (equivalence_associated f).
Proof. 
move=>  ff.
have sr := proj2(graph_ea_equivalence ff).
by split=> // x x' /(ea_relatedP ff) [_ _]. 
Qed.

Lemma ea_foq_fi f:
  function f ->
  injection (fun_on_quotient (equivalence_associated f) f).
Proof. 
move=>  ff.
case:(graph_ea_equivalence ff).
set (g:= equivalence_associated f) => eg sf.
split; first by apply: foqc_f.
have: source (fun_on_quotient g f) = (quotient g)
  by rewrite/fun_on_quotient/section_canon_proj; aw. 
move => -> x y xq yq.
rewrite  foqc_V // foqc_V // => h. 
move: (rep_i_sr eg xq) (rep_i_sr eg yq) => xs ys. 
have: (related g (rep x) (rep y))  by  apply/(ea_relatedP ff);rewrite - sf.
by move/related_rr_P; apply.
Qed.

Lemma ea_foq_on_im_fb f:
  function f ->
  bijection (restriction2 (fun_on_quotient (equivalence_associated f) f)
    (quotient (equivalence_associated f)) (range (graph f))).
Proof. 
move=> ff.
case:(graph_ea_equivalence ff).
set (g:= equivalence_associated f) => eg sfsg.
set (h:= fun_on_quotient g f).
have ih: injection h by rewrite /h/g; apply: ea_foq_fi. 
have fh: function h by  fct_tac.
have qg: quotient g = source h.
   by rewrite /h/fun_on_quotient/section_canon_proj; aw.
have aux: sub (quotient g) (source h)  by rewrite qg.
suff rg: range (graph f) =  Vfs h (quotient g). 
  rewrite rg qg restriction1_pr //.
  apply: restriction1_fb; fprops.
set_extens t.
  move /(range_fP ff) => [x xsf ->].
  rewrite - sfsg in xsf.
  have gxq: inc (class g x) (quotient g) by fprops.
  apply /(Vf_image_P fh aux); exists (class g x) => //.
  have : (related g x (rep (class g x))) by  apply: related_rep_class.
  move / (ea_relatedP ff x (rep (class g x))) => [pa pb ->].
  rewrite - (foqc_V eg) //;Wtac. 
move /(Vf_image_P fh aux)=> [u us ->].
by rewrite foqc_V //; Wtac; rewrite - sfsg; apply: rep_i_sr.
Qed.

(** Canonical decomposition of a function as a surjection, a bijection and an ionjection  *)

Lemma canonical_decompositiona f (r:= equivalence_associated f):
  function f ->
    function ((restriction2 (fun_on_quotient r f)
      (quotient r) (range (graph f))) 
     \co (canon_proj r)).
Proof. 
move=> ff.
set (g:= canon_proj r). 
set (a:=range (graph f)).
set (j:=canonical_injection a (target f)).
set (k:=restriction2 (fun_on_quotient r f) (quotient r) a).
have [er sr]:= (graph_ea_equivalence ff).
have sat: sub a (target f) by apply: f_range_graph.  
have fj: function j by  apply: ci_f.
have ffo: function (fun_on_quotient r f) by apply: foqc_f.
have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) a.
  hnf;rewrite{2 3}/fun_on_quotient/section_canon_proj; aw;split => //.
  move => x /(dirim_P) [z zq zj].
  rewrite (Vf_pr ffo zj) foqc_V //; apply/range_fP => //. 
  exists (rep z) => //; rewrite - sr; fprops.
have fk:function k by rewrite /k; apply: (proj31 (restriction2_prop ra)).
have ckg: k \coP g.
  rewrite  /k/g; split; fprops; rewrite /restriction2;aw. 
fct_tac.
Qed.

Lemma canonical_decomposition f (r:= equivalence_associated f):
  function f ->
  f = (canonical_injection (range (graph f))(target f))
      \co (restriction2 (fun_on_quotient r f) (quotient r) (range (graph f))
           \co (canon_proj r)).
Proof.
move=> ff.
set (g:= canon_proj r). 
set (a:=range (graph f)).
set (j:=canonical_injection a (target f)).
set (k:=restriction2 (fun_on_quotient r f) (quotient r) a).
have [er sr]:= (graph_ea_equivalence ff).
have sat: sub a (target f) by rewrite /a ; apply: f_range_graph.  
have fj:function j by rewrite /j;apply: ci_f.
have foq: function (fun_on_quotient r f) by apply: foqc_f.
have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) a.
  hnf;rewrite{2 3}/fun_on_quotient/section_canon_proj; aw;split => //.
  move => x /(dirim_P) [z zq zj].
  rewrite (Vf_pr foq zj) foqc_V //; apply/range_fP => //. 
  exists (rep z) => //; rewrite - sr; fprops.
move: (proj31 (restriction2_prop ra)) => fr.
have fk:function k by rewrite /k.
have ckg:k \coP g.
  rewrite /k/g; split; fprops; rewrite /restriction2;aw. 
have sfg: source f = source g by rewrite /g; aw.
have fkg: function (k \co g) by fct_tac. 
have cjkg: j \coP (k \co g).
  by split => //; rewrite/j/k/canonical_injection/restriction2; aw.
apply: function_exten=>//; try fct_tac; aw.
  by rewrite/j/canonical_injection; aw.
move=> x xsf.
  move: (xsf); rewrite - sr=> xsr; rewrite sfg in xsf.
  have a1: (quotient r = target g) by rewrite /g;aw.
  have W1q: inc (Vf g x) (quotient r) by Wtac; fct_tac.
  have p1: inc (Vf k (Vf g x)) a.
    have ->: (a = target k) by rewrite/k/restriction2; aw.
    by Wtac; rewrite /k/restriction2; aw; ue.
aw. 
rewrite /j ci_V // /k restriction2_V // foqc_V // /g; aw.
have : (related r x (rep (class r x))) by apply: related_rep_class.
by move/(ea_relatedP ff) => [_ _].
Qed.


Lemma surjective_pr7 f:
  surjection f -> 
  canonical_injection (range (graph f))(target f) = identity (target f).
Proof. 
move=> sf; rewrite surjective_pr3 //.
Qed.

Lemma canonical_decomposition_surj f (r:= equivalence_associated f):
  surjection f ->
  f =  (restriction2 (fun_on_quotient r f) (quotient r) (target f))
       \co (canon_proj r).
Proof. 
move=> sf.
move: (surjective_pr7 sf)  (surjective_pr3 sf) => p1 p2.
move: sf => [sf _].
move: (canonical_decomposition sf); rewrite /= p1 p2 -/r => {1} ->.
set (g:= (restriction2 (fun_on_quotient r f) (quotient r) (target f))).
set (h:= g \co (canon_proj r)).
have fh: function h by move:(canonical_decompositiona sf); rewrite -/r p2.
have -> : (target f = target h) by rewrite /h/g/restriction2; aw.
by apply:compf_id_l.
Qed.

Lemma canonical_decompositionb f (r:= equivalence_associated f):
  function f ->
    restriction2 (fun_on_quotient r f)  (quotient r) (target f) =
    (fun_on_quotient r f).
Proof. 
move=> ff.
set (k:=restriction2 (fun_on_quotient r f) (quotient r) (target f)).
have [er sr]:= (graph_ea_equivalence ff).
have ffoq: function (fun_on_quotient r f) by apply: foqc_f.
have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) (target f).
  hnf;rewrite{2 3}/fun_on_quotient/section_canon_proj; aw;split => //.
  move => x /(dirim_P) [z zq zj].
  rewrite (Vf_pr ffoq zj) foqc_V //; Wtac; rewrite - sr;fprops.
have fk: function k by rewrite /k; apply: (proj31(restriction2_prop ra)).
have sk: source k = quotient r by rewrite /k/restriction2; aw.
apply: function_exten =>//.
- rewrite /restriction2/fun_on_quotient/section_canon_proj; aw.
- by rewrite/k/restriction2/fun_on_quotient; aw. 
- move=> x; rewrite sk => xq; rewrite restriction2_V //. 
Qed.

Lemma canonical_decomposition_surj2 f (r:= equivalence_associated f):
  surjection f ->
  f =  (fun_on_quotient r f) \co (canon_proj r).
Proof.
move=> sf; move: (canonical_decomposition_surj sf). 
by move: sf => [ff _]; move: (canonical_decompositionb ff) => /= -> <-.
Qed.

(** **  EII-6-6 Inverse image of an equivalence relation; induced equivalence relation *)

(** We have an equivalence on the source induced by the equivalence on the target*)

Definition inv_image_relation f r :=
  equivalence_associated (canon_proj r \co f). 

Definition iirel_axioms f r :=
  [/\ function f, equivalence r & substrate r = target f].

Lemma iirel_f f r:
   iirel_axioms f r -> function (canon_proj r \co f).
Proof. 
move=> [ff er tf]; fct_tac; [ fprops | aw].
Qed.

Lemma iirel_relation f r:
  iirel_axioms f r -> equivalence_on (inv_image_relation f r) (source f).
Proof. 
move=> ia;move:(graph_ea_equivalence(iirel_f ia)); aw.
Qed.

Lemma iirel_relatedP f r:  iirel_axioms f r ->  forall x y,
  (related (inv_image_relation f r) x y <->
   [/\ inc x (source f), inc y (source f) & related r (Vf f x) (Vf f y)]). 
Proof. 
move=> ia.
have fc : function ((canon_proj r) \co f) by apply: iirel_f.
move: ia => [ff er tf].
rewrite /inv_image_relation.
have cct: ((canon_proj r) \coP f) by split; fprops; aw.
have iWs: forall u, inc u (source f) -> inc (Vf f u) (substrate r).
  by move=> u; rewrite tf; fprops. 
move => x y.
split.
  move/(ea_relatedP fc); rewrite compf_s; move => [xs ys].
  move: (iWs _ xs) (iWs _ ys)=> p1 p2; aw => p3;split => //.
  by apply/(related_equiv_P er).
move => [pa pb pc].
apply /(ea_relatedP fc); split; aw; fprops;apply: class_eq1;fprops.
Qed.

Lemma iirel_classP f r:
  iirel_axioms f r -> forall x, 
  (classp (inv_image_relation f r) x  <->
  exists y, [/\ classp r y,
    nonempty (y \cap (range (graph f)))
    & x = Vfi f y]).
Proof. 
move=> ia; move: (ia) => [ff er tf].
have [pa sir] := (iirel_relation ia).
move => x; split.
  move => clix; move: (clix)=> []; rewrite sir => sa sb.
  have iWs: inc (Vf f (rep x)) (substrate r) by rewrite tf;  Wtac.
  exists (class r (Vf f (rep x))); split.
  - by apply: class_class.
  - exists (Vf f (rep x)); apply: setI2_i; [ fprops | Wtac ].
  - set_extens t.
    rewrite {1} sb => /(class_P pa)  /(iirel_relatedP ia) [ysf tsf ryt].
    apply/(iim_fun_P); exists (Vf f t); [ by apply /class_P | Wtac].
  move /(iim_fun_P) => [u uc Jg]; rewrite sb; apply /(class_P pa).
  apply /(iirel_relatedP ia);split => //; first by Wtac.
  by rewrite - (Vf_pr ff Jg); apply /(class_P er).
move=> [y [cy [u ui] xi]]; move: cy => [c1 c2].
move: ui => /setI2_P [uy] /(range_fP ff) [v vsf uw].
have vx: inc v x by rewrite xi; apply /(iim_fun_P); ex_tac; rewrite uw; Wtac.
have qc: related r (rep y) (Vf f v) by rewrite - uw;apply /class_P => //; ue.
suff: x = class (inv_image_relation f r) v.
  move => ->; apply: class_class => //; ue.
set_extens t.
  rewrite  xi => /(iim_fun_P) [z' z'y Jg2].
  apply/(class_P pa); apply /(iirel_relatedP ia);split => //; first by Wtac.
  have pb: related r (rep y) z' by apply /(class_P er); ue.
  rewrite - (Vf_pr ff Jg2); equiv_tac.
move /(class_P pa) => /(iirel_relatedP ia)  [_ qa qb].
rewrite xi; apply /(iim_fun_P); exists (Vf f t) => //; last by  Wtac. 
rewrite c2; apply /class_P => //; equiv_tac.
Qed.

(** Equivalence induced on a subset of the substrate *)

Definition induced_relation r a :=
  inv_image_relation (canonical_injection a (substrate r)) r.

Definition induced_rel_axioms r a  :=
   equivalence r /\ sub a (substrate r).
Definition canonical_foq_induced_rel r a :=
  restriction2 (fun_on_quotients (induced_relation r a) r 
    (canonical_injection a (substrate r))) 
  (quotient (induced_relation r a))
  (Vfs (canon_proj r) a).

Section InducedRelation.
Variables (r a: Set).
Hypothesis ira: induced_rel_axioms r a. 

Lemma induced_rel_iirel_axioms:
  iirel_axioms (canonical_injection a (substrate r)) r.
Proof.
move: ira=> [er ar]; split; fprops;rewrite/canonical_injection; aw.
Qed.

Lemma induced_rel_equivalence:
  equivalence_on (induced_relation r a) a.
Proof.
move: (iirel_relation induced_rel_iirel_axioms).
rewrite/canonical_injection; aw. 
Qed.


Lemma induced_rel_relatedP u v:
  related (induced_relation r a) u v <->
    [/\ inc u a, inc v a & related r u v].
Proof. 
move: (induced_rel_iirel_axioms) => iia.
move: ira=> [er ar].
split.
  move/(iirel_relatedP iia); rewrite lf_source; move => [pa pb].
  rewrite ci_V //ci_V  //.
move => [ua va ruv];apply/(iirel_relatedP iia); rewrite lf_source; split => //.
rewrite ci_V //ci_V  //. 
Qed.

Lemma induced_rel_classP x:
  (classp (induced_relation r a) x <->
  exists y, [/\ classp r y, nonempty (y \cap a) & x = (y \cap a)]).
Proof. 
have iia:=(induced_rel_iirel_axioms).
move: (ira)=> [er ar].
have p: forall y, Vfi (canonical_injection a (substrate r)) y
   = y \cap a.
  rewrite/Vfi /canonical_injection; aw.
  rewrite - diagonal_is_identity.
  move=> y;set_extens t.
    move /iim_graph_P => [u uy] /diagonal_pi_P [pa pb]; apply/setI2_P.
    split => //; ue.
  move /setI2_P => [ty ta]; apply /iim_graph_P; ex_tac. 
  by apply /diagonal_pi_P.
split.
  move/(iirel_classP iia); rewrite (ci_range ar); move => [y]; rewrite p.
  by move => [pa pb pc]; exists y.
move => [y [cy ney xi]]; apply/(iirel_classP iia); exists y.
split; [ done |  by rewrite (ci_range ar) | by rewrite p ].
Qed.

Lemma compatible_injection_induced_rel:
  compatible_with_equivs (canonical_injection a (substrate r))
  (induced_relation r a) r.
Proof. 
move: (ira)=> [er sa].
move:(induced_rel_equivalence) => [qa qb].
apply: compatible_with_pr2 =>//.
- by apply: ci_f.
- rewrite/canonical_injection; aw. 
- by rewrite/canonical_injection;aw.
- move=> x y /induced_rel_relatedP [xa ya rxy]; rewrite ci_V // ci_V //. 
Qed.

Lemma foq_induced_rel_fi:
  injection (fun_on_quotients (induced_relation r a) r 
    (canonical_injection a (substrate r))).
Proof.
move: (ira)=> [er sa].
set (f := (canonical_injection a (substrate r))).
have [ei sr] := (induced_rel_equivalence).
have ff: function f by rewrite /f;apply: ci_f.
have tf: target f = substrate r by rewrite /f /canonical_injection; aw.
have sf: source f = substrate (induced_relation r a).  
  rewrite /f sr // /canonical_injection; aw.
split; first by apply: foqcs_f. 
have ->: (source (fun_on_quotients (induced_relation r a) r f) = 
    quotient (induced_relation r a) ).
  rewrite/fun_on_quotients /section_canon_proj; aw. 
move=> x y xs ys /=; rewrite  foqcs_V // foqcs_V //.
have eq: a = substrate (induced_relation r a) by rewrite sr.
have rxa: inc (rep x) a by rewrite eq; fprops.
have rya: inc (rep y) a by rewrite eq; fprops.
rewrite ci_V //  ci_V // => cc.
have: (related (induced_relation r a) (rep x) (rep y)).
  apply /induced_rel_relatedP; split => //; apply/ related_equiv_P => //.
   by split => //; apply: sa. 
by move /(related_rr_P ei xs ys).
Qed.

Lemma foq_induced_rel_image :
  Vfs  (fun_on_quotients (induced_relation r a) r 
    (canonical_injection a (substrate r))) (quotient (induced_relation r a))
  = Vfs (canon_proj r) a.
Proof. 
move: (ira)=> [er sa].
set (ci := canonical_injection a (substrate r)).
have fci: function ci by apply: ci_f.
have [ei qb] := induced_rel_equivalence.
have sci: source ci = substrate (induced_relation r a).
  rewrite qb /ci  /canonical_injection; aw.
set (f:= fun_on_quotients (induced_relation r a) r ci).
move: (foq_induced_rel_fi); rewrite -/ci -/f; move => inf.
have ff: function f by fct_tac. 
have gf: sgraph (graph f) by fprops.
have tci: target ci = substrate r by rewrite /ci/canonical_injection; aw.
have fc: function (canon_proj r) by fprops.
set_extens x. 
  move/dirim_P => [y yq Jg].
  move: (yq) => /(setQ_P ei) /induced_rel_classP [z [cz nei yi]].
  move: (Vf_pr ff Jg); rewrite foqcs_V // => cx. 
  have: (inc (rep y) (z \cap a)) by rewrite -yi; apply: (setQ_repi ei).
  move /setI2_P => [ryz rya]; rewrite  ci_V // in cx. 
  move: nei=> [u] /setI2_P [uz ua]; apply /dirim_P; ex_tac.
  have ryu: (related r (rep y) u) by apply/(in_class_relatedP er); exists z.
  move: (sa _ ua) => us.  
  have ->: x = Vf (canon_proj r) u by aw; rewrite cx; apply: class_eq1.
  by Wtac; aw.
move/dirim_P => [y ya Jg]; move: (sa _ ya)=> yu.
move: (Vf_pr fc Jg); aw; move => cx.
have yx: (inc y x) by rewrite cx; fprops.
set (z:= x \cap a).
have ney: nonempty z by rewrite /z; exists y; fprops. 
have zq: inc z (quotient (induced_relation r a)).
  apply/(setQ_P ei); apply/ induced_rel_classP; exists x; split => //.
   rewrite cx; apply: class_class =>//. 
apply /dirim_P; ex_tac.
have: (inc (rep z) (x \cap a)) by apply: (setQ_repi ei).
move /setI2_P => [rzx rza].
have -> : x = Vf f (x \cap a).  
  rewrite /f foqcs_V// ci_V // -/z cx.  
  have:  (related r y (rep z)). 
    apply /(in_class_relatedP er); exists x; split => //.
    by rewrite cx; apply: class_class.
  by move /(related_equiv_P er) => [_ _].
rewrite -/z; Wtac; rewrite/f/fun_on_quotients/section_canon_proj; aw.
Qed. 

Lemma canonical_foq_induced_rel_fb:
 bijection (canonical_foq_induced_rel r a).
Proof.
set ci:= (canonical_injection a (substrate r)).
have sf: source (fun_on_quotients (induced_relation r a) r ci) = 
     quotient (induced_relation r a).
  rewrite /fun_on_quotients/section_canon_proj; aw.
have ra:restriction2_axioms
     (fun_on_quotients (induced_relation r a) r ci)
     (quotient (induced_relation r a)) (Vfs (canon_proj r) a).
  move: (foq_induced_rel_fi) => ifoq. 
  split; first by fct_tac.
     by rewrite /fun_on_quotients/section_canon_proj; aw.
    rewrite /fun_on_quotients; aw; move=> t ts; move: ira=> [er ar].
    apply: (sub_im_canon_proj_quotient  ar ts). 
  by rewrite foq_induced_rel_image; fprops.
split; first  by apply: restriction2_fi=>//; apply: foq_induced_rel_fi.
apply: restriction2_fs=>//.
by rewrite - foq_induced_rel_image /Imf sf.
Qed.

End InducedRelation.

(** ** EII-6-7 Quotients of equivalence relations *)

(** Definition of a finer equivalence *)

Definition finer_equivalence s r:= 
  forall x y, related s x y -> related r x y.

Definition finer_axioms s r := 
  [/\ equivalence s,  equivalence r & substrate r = substrate s].

Lemma finest_equivalence r:
   equivalence r -> finer_equivalence (diagonal (substrate r)) r.
Proof. move=> er x t /diagonal_pi_P [xs <-]; equiv_tac. Qed.

Lemma coarsest_equivalence r:
   equivalence r -> finer_equivalence r (coarse (substrate r)).
Proof. 
move=>  er x y;rewrite coarse_related; move /(related_equiv_P er) => [pa pb _].
by split.
Qed.

Section FinerEquivalence.
Variable (r s: Set).
Hypothesis fa: finer_axioms s r.

Lemma finer_sub_equivP:
  (finer_equivalence s r <-> sub s r).
Proof. 
move: fa => [es er srss].
split. 
  move=> fe t ts. 
  have gs: (sgraph s) by fprops. 
  by rewrite -(gs _ ts); apply: fe; hnf; rewrite (gs _ ts).
move => t x y; rewrite /related; apply: t.
Qed.

Lemma finer_sub_equivP2:
  (finer_equivalence s r <-> 
    (forall x, exists y, sub (class s x) (class r y))).
Proof.
move: fa=> [es er srss].
split. 
  move=> fsr x; exists x. 
  by move=> u /(class_P es) h; apply /(class_P er); apply:fsr.
move=> h x y rxy.
move:(h x)=> [z sxz]. 
have xs: inc x (substrate s) by substr_tac.
have ixc: inc x (class s x) by fprops.
have ys: inc y (class s x) by apply /(class_P es).
move: (sxz _ ixc)(sxz _ ys) => /(class_P er) pa /(class_P er) pb; equiv_tac.
Qed.

Lemma finer_sub_equivP3:
  (finer_equivalence s r <-> forall y, saturated s (class r y)).
Proof. 
move: (fa)=>[es er srss].
split.  
  move=> fe y.
  apply/(saturatedP es); first by  rewrite - srss; apply: sub_class_substrate. 
  move => z zc; move: fe => /finer_sub_equivP2 fe.
  move/(class_P er): (zc) => r1.
  have zs: (inc z (substrate s)) by rewrite - srss; substr_tac.
  move: (fe z)=> [x cxy]. 
  suff: (class r x = class r y) by move=> <-.
  have: (inc z (class r x)) by apply: cxy; fprops.
  move =>  /(class_P er) r2.
  apply: (class_eq1 er); equiv_tac.
move=> p x y re; move: (p x).
move: (sub_class_substrate er (x:=x)); rewrite  srss => aux.
move /(saturatedP es aux) => h.
have p1: inc x (substrate s) by substr_tac.
have p2: inc x (class r x) by rewrite - srss in p1;fprops.
have p3: inc y (class s x) by apply/class_P.
by move:((h  _ p2) _ p3) => /(class_P er).
Qed.

Lemma compatible_with_finer:
  finer_equivalence s r -> 
  compatible_with_equiv (canon_proj r) s.
Proof. 
move :fa=> [es er fh] fe.
split; fprops; aw => x y rxy.
move: (fe _ _ rxy) => /(related_equiv_P er) [p1 p2 h];  aw.  
Qed. 

Lemma foq_finer_f:
  finer_equivalence s r -> function(fun_on_quotient s (canon_proj r)).
Proof. move : fa=> [es er fh] fe;  apply: foqc_f; fprops; aw. Qed.

Lemma foq_finer_V x:
  finer_equivalence s r ->  inc x (quotient s) ->
  Vf (fun_on_quotient s (canon_proj r)) x = class r (rep x).
Proof. 
move: fa => [es er fh] fe xq; rewrite  foqc_V //; aw; fprops. 
rewrite fh; fprops. 
Qed.

Lemma foq_finer_fs:
  finer_equivalence s r -> surjection(fun_on_quotient s (canon_proj r)).
Proof. 
move=> fe.
split; first by apply: foq_finer_f.
move: fa=> [es er ss] y yt.
have yq:inc y (quotient r) by  move:yt; rewrite/fun_on_quotient; aw.
have rys:(inc (rep y) (substrate r)) by fprops.
have sfo:source (fun_on_quotient s (canon_proj r)) = (quotient s).
  by rewrite /fun_on_quotient/section_canon_proj; aw.
set(x := class s (rep y)). 
have xq: (inc x (quotient s)) by rewrite /x; rewrite ss in rys; fprops. 
rewrite sfo; ex_tac.
rewrite foq_finer_V //. 
have cry: (class r (rep y) = y) by apply: class_rep=>//. 
rewrite -cry; apply: class_eq1 =>//;apply: fe.
apply: (symmetricity_e es).
apply /(class_P es); apply: rep_i; rewrite /x. 
apply /(setQ_ne es); apply /(setQ_P es); apply/(class_class es); ue.
Qed.

End FinerEquivalence.

(** Quotient of a relation by a finer one *)

Definition quotient_of_relations r s:= 
  equivalence_associated (fun_on_quotient s (canon_proj r)).

Lemma cqr_aux s x y u:
  equivalence s -> sub y (substrate s) -> 
  x = Vfs (canon_proj s) y ->
  (inc u x <-> (exists2 v, inc v y & u = class s v)).
Proof. 
move=> es ys xi.
split.
  rewrite xi /Vfs => ui.
  move:(sub_im_canon_proj_quotient  ys ui) => uqs.
  move: ui=> /dirim_P [z zy Jg]; move : (ys _ zy) => zs. 
  move: Jg => /(rel_gcp_P es zs uqs) zu.
  ex_tac.
  have aux: (class s (rep u) = u) by (apply: class_rep). 
  have : related s (rep u) z by apply /(class_P es); ue.
  move /(related_equiv_P es) => [_ _]; ue.
have fc: function (canon_proj s) by fprops. 
move=> [v vy ->]; move: (ys _ vy) => vs; rewrite xi.
apply/dirim_P; ex_tac; apply /(rel_gcp_P es vs); fprops. 
Qed.

Section QuotientRelations.
Variables (r s: Set).
Hypotheses (fa:finer_axioms s r) (fe: finer_equivalence s r).

Lemma quo_rel_equivalence: 
  equivalence_on (quotient_of_relations r s) (quotient s).
Proof. 
move: (graph_ea_equivalence (proj1 (foq_finer_fs fa fe))). 
rewrite/fun_on_quotient/section_canon_proj; aw.
Qed.


Lemma quo_rel_relatedP x y:
  related (quotient_of_relations r s) x y <->
    [/\ inc x (quotient s), inc y (quotient s) & related r (rep x) (rep y)].
Proof.
have foq: function (fun_on_quotient s (canon_proj r)).
  by apply:(surj_function (foq_finer_fs fa fe)).
have fc: function (canon_proj r) by fprops.
have sf: source (fun_on_quotient s (canon_proj r)) = quotient s.
  rewrite /fun_on_quotient/section_canon_proj; aw. 
move: fa =>[es er ss].
have sc:source (canon_proj r) = substrate s by aw.
rewrite/quotient_of_relations; split.
  move /(ea_relatedP foq); rewrite sf.
  move => [xq yq h];split => //.
  have p1: (inc (rep x) (substrate r)) by rewrite ss; fprops.
  have p2: (inc (rep y) (substrate r)) by rewrite ss; fprops.
  move: h;rewrite foqc_V // foqc_V //; aw => h.
  by apply/(related_equiv_P er).
move => [xs ys rr]; apply /(ea_relatedP foq); rewrite sf; split => //.
move/(related_equiv_P er): rr => [p1 p2 p3].
rewrite foqc_V //  foqc_V //; aw.
Qed.

Lemma quo_rel_related_bisP  x y:
  inc x (substrate s) -> inc y (substrate s) ->
  (related (quotient_of_relations r s) (class s x) (class s y)
     <-> related r x y).
Proof. 
move=> xs ys.
move: fa =>[es er ss].
have p1:(related r x (rep (class s x))) by apply: fe; apply: related_rep_class.
have p2:(related r y (rep (class s y))) by apply: fe; apply: related_rep_class.
split.
  move/quo_rel_relatedP=> [ixs iys rxy].
  apply: (@transitivity_e _ (rep (class s x))) =>//.
  apply: (@transitivity_e _  (rep (class s y))) =>//. 
  equiv_tac.
move=> h; apply/quo_rel_relatedP; split; fprops.
apply: (@transitivity_e _  x) =>//.
apply: symmetricity_e=>//. 
equiv_tac. 
Qed.

Lemma quo_rel_class_bisP x:
  ( inc x (quotient (quotient_of_relations r s)) <->
    exists2 y, inc y (quotient r) & x = Vfs (canon_proj s) y).
Proof. 
have [eq aux ]:=(quo_rel_equivalence).
move: (fa) =>[es er ss]. 
have fc: function (canon_proj s) by fprops.
split.
  move/(setQ_P eq) => cq; move: (cq)=> [ca cb].
  set(y:= Zo (substrate r) (fun v => exists2 u, inc u x & inc v u)).
  move: (rep_in_class eq cq) => rxx.
  move: (sub_class_sr eq cq); rewrite aux => scx.
  move: (scx _ rxx) => repxq; move: (setQ_repi es repxq) => rrx.
  have rrsr: inc (rep (rep x)) (substrate r).
    by rewrite ss; apply: (inc_in_setQ_sr es rrx repxq).
  have ys: sub y (substrate r) by rewrite /y ss; apply: Zo_S.
  have cy: y = class r (rep (rep x)).
    set_extens u.
       move /Zo_P => [usr [t tx ut]]; apply /(class_P er).
       move: tx; rewrite {1} cb; move /(class_P eq).
       move /quo_rel_relatedP => [uq vq ruv].
       apply: (@transitivity_e _ (rep t))=>//.
       by apply: fe; apply/(class_P es); rewrite class_rep.
    move /(class_P er) => rab.
    move: (arg2_sr rab) => bsr; move: rab.
    rewrite ss in rrsr bsr.
    move /(quo_rel_related_bisP rrsr bsr).
    move /(class_P eq); rewrite (class_rep es repxq) - cb => h.
    apply: Zo_i; [ ue | ex_tac].
  exists y.
    rewrite cy; apply/(setQ_P er); apply: (class_class er rrsr).
  set (xx := Vfs (canon_proj s) y). 
  rewrite ss in ys.
  set_extens u. 
    move => ux; move: (scx _ ux) => aux1; 
    apply/ (cqr_aux u es ys (refl_equal xx)).
    move: (setQ_repi es aux1) => ur.
    exists (rep u); first by apply: Zo_i; [ ue | ex_tac].
    by symmetry; apply: class_rep.
  move/ (cqr_aux u es ys (refl_equal xx)) => [v vy ->].
  move: vy => /Zo_P [vr [w wx vw]].
  have wq: (inc w (quotient s)) by apply: scx.
  move: (related_rep_in_class es wq vw).
  move => /(related_equiv_P es) [rws vd]. 
  by move: (class_rep es wq) => -> <-.
move =>  [y] /(setQ_P er) cy xd; apply /(setQ_P eq).
move: (rep_in_class er cy) => ryy.
move: (sub_class_sr er cy); rewrite ss => ysr.
have sxq: sub x (quotient s).
   by move => t tx; apply: (sub_im_canon_proj_quotient ysr); ue.
have nex: nonempty x by rewrite xd; apply: nonempty_image => //; aw; ex_tac.
move: (rep_i nex) => rrx.
move: (rrx) => /(cqr_aux (rep x) es ysr xd) [v vy asv].
split; [ue |  set_extens t].
  move => tx; apply/(class_P eq).
  move/ (cqr_aux t es ysr xd): tx => [w wy asw].
  rewrite asv asw ; apply /quo_rel_related_bisP; try apply: ysr => //.
  by apply /(in_class_relatedP er); exists y.
move /(class_P eq) => /quo_rel_relatedP [aq bq rab].
apply/(cqr_aux t es ysr xd); exists (rep t); last by symmetry; apply: class_rep.
move: (rel_in_class er cy vy) => s1.
apply: (rel_in_class2 er cy).
apply: (transitivity_e er s1).
apply: (@transitivity_e _ (rep (rep x)))=>//.
apply: fe; apply /(in_class_relatedP es).
exists (rep x); split.
- by rewrite asv; apply: class_class =>//; apply: ysr.
- by rewrite asv; apply: inc_itself_class =>//; apply: ysr.
- by apply: (setQ_repi es).
Qed.


Lemma quotient_canonical_decomposition
   (f := fun_on_quotient s (canon_proj r))
   (qr := quotient_of_relations r s):
  f =  (fun_on_quotient qr f) \co (canon_proj qr).
Proof.
have sj: (surjection f) by rewrite /f;apply: foq_finer_fs.
apply: (canonical_decomposition_surj2 sj).
Qed.

End QuotientRelations.

Lemma quo_rel_pr s t
  (r := inv_image_relation (canon_proj s) t):
  equivalence s -> equivalence t -> substrate t = quotient s ->
  t = quotient_of_relations r s.
Proof. 
move=> es et st.
have iaa: iirel_axioms (canon_proj s) t. 
  by split;fprops; aw.
have [er sr]:=(iirel_relation iaa).
have fa:finer_axioms s r.
  by split=>//; rewrite /r sr //; aw.
have fe: finer_equivalence s r. 
  move => x y sxy; apply / iirel_relatedP =>  //. 
  have xs: inc x (substrate s) by  substr_tac.
  have ys: inc y (substrate s) by  substr_tac.
  aw;split=>//.
  have -> : (class s x =class s y) by  apply: class_eq1.
  by apply: reflexivity_e=>//; rewrite st; fprops.
have [eq sr'] := (quo_rel_equivalence fa fe).
apply/sgraph_exten; fprops.
move=> u v; split.
  move => tuv; apply/quo_rel_relatedP => //.
  have us: (inc u (quotient s))  by rewrite - st; substr_tac.
  have vs: (inc v (quotient s))  by rewrite - st; substr_tac.
  have rus: (inc (rep u) (substrate s)) by fprops.
  have rvs: (inc (rep v) (substrate s)) by fprops.
  split=>//; apply /iirel_relatedP => //.
  by split; aw; rewrite class_rep // class_rep.
move/(quo_rel_relatedP fa fe) => [uq vq]. 
move /(iirel_relatedP iaa) ;rewrite canon_proj_s. 
move=> [ru rv]; aw; rewrite class_rep // class_rep //.  
Qed.

(** ** EII-6-8 Product of two equivalence relations *)

Definition prod_of_relation r r':=
  graph_on 
    (fun x y=> inc (J(P x)(P y)) r /\ inc (J(Q x)(Q y)) r')
  ((substrate r) \times (substrate r')).

Lemma substrate_prod_of_rel r r':
  equivalence r ->equivalence r' ->
  substrate (prod_of_relation r r') =  (substrate r)\times (substrate r').
Proof.
move => pa pb; rewrite graph_on_sr //.
by move => a /setX_P [_ ta tb]; split; equiv_tac.
Qed.

Lemma order_product2_sr1 f g:
  preorder f -> preorder g -> 
  substrate (prod_of_relation f g) = (substrate f) \times (substrate g).
Proof. 
move=> [_ rf _] [_ rg _ ]; apply: graph_on_sr. 
move => a /setX_P [pa Ps Qs]. 
by split; [apply: rf | apply: rg].
Qed.

Lemma order_product2_sr f g:
  order f -> order g -> 
  substrate (prod_of_relation f g) = (substrate f) \times (substrate g).
Proof.
move=> orf og; apply: order_product2_sr1; by apply: order_preorder.
Qed.

Lemma equivalence_prod_of_rel r r':
  equivalence r -> equivalence r' ->
  equivalence (prod_of_relation r r').  
Proof.
move => pa pb.
apply: equivalence_from_rel; split.
  move => a b [ra rb];split; equiv_tac.
move => a b c [ra rb] [rc rd];split; equiv_tac.
Qed. 

Lemma order_product2_preorder f g:
  preorder f -> preorder g -> preorder (prod_of_relation f g).
Proof.
move => [_ rf tf] [_ rg tg]; apply: preorder_from_rel; hnf; split.
  move => x y z[pxy qxy][pyz qyz].  
  split; [ apply: tf pxy pyz | apply: tg qxy qyz].
move=> x y [pxy qxy]; split; split; try apply: rf; try apply: rg; substr_tac.
Qed.

Lemma order_product2_or f g:
  order f -> order g -> order (prod_of_relation f g).
Proof. 
move=> orf og.
have [gr rr tr]: preorder (prod_of_relation f g).
  by apply: order_product2_preorder;  apply: order_preorder.
move: orf og => [_ rf tf af] [_ rg tg ag].
split => //.
move => x y /Zo_P [pa [pb pc]] /Zo_P [qa [qb qc]].
move: pb pc qb qc; aw => pb pc qb qc.
move: pa => /setX_P [_ ]; aw ;move /setX_P => [px _ _] /setX_P [py _ _].
apply: pair_exten => //; [exact: (af _ _ pb qb) | exact: (ag _ _ pc qc)].
Qed.

Lemma prod_of_rel_P r r' a b:
  related (prod_of_relation r r')  a b <->
  [/\ pairp a, pairp b, related r (P a) (P b) & related r' (Q a) (Q b)].
Proof.
rewrite /related /prod_of_relation; split.
  by move /graph_on_P0 =>  [] /setX_P [pa _ _]  /setX_P [pb _ _] [pc pd].
move => [pa pb pc pd]; apply /graph_on_P0;split => //;
  apply/setX_P; split => //; substr_tac.
Qed.

Lemma related_prod_of_relP1  r r' x x' v:
 related (prod_of_relation r r') (J x x') v <->
   (exists y y', [/\ v = J y y',  related r x y & related r' x' y']).
Proof.
split.
  move /prod_of_rel_P; aw; move=> [_ pb pc pd].
  by exists (P v); exists  (Q v).
move=> [y [y' [eq r1 r2]]]; rewrite eq; apply /prod_of_rel_P; aw; split; fprops.
Qed.

Lemma related_prod_of_relP2 r r' x x' v:
  (related (prod_of_relation r r') (J x x') v <->
    inc v ((im_of_singleton r x) \times (im_of_singleton r' x'))).
Proof. 
split. 
  move=> /related_prod_of_relP1 [y [y' [eq r1 r2]]]; rewrite eq. 
  by apply/setXp_i; apply /dirim_set1_P.
move /setX_P => [pv /dirim_set1_P j1r /dirim_set1_P j2r]. 
by apply/related_prod_of_relP1;exists (P v); exists (Q v);aw.
Qed.

Lemma class_prod_of_relP2 r r':
  equivalence r -> equivalence r' -> forall x,
  (classp (prod_of_relation r r') x  <->
    exists u v, [/\ classp r u, classp r' v & x = u \times v]).
Proof.
move=> er er'.
move:(equivalence_prod_of_rel er er')=> er''.
split.
  move => cx; move: (cx) => [ca cb].
  move: (ca); rewrite (substrate_prod_of_rel er er') => /setX_P [pa pb pc].
  exists (class r (P (rep x))); exists (class r' (Q (rep x))); split => //.
    by apply: (class_class er).
    by apply: (class_class er').
  set_extens v.
    rewrite {1} cb; move /(class_P er'') => /prod_of_rel_P [qa qb qc qd].
    apply /setX_P => //; split => //; apply /class_P => //.
  move /setX_P => [qa qb qc]; rewrite cb; apply /(class_P er'').
  by apply /prod_of_rel_P;split => //; apply /class_P.
move=> [u [v [pa pb pe]]].
move: (pa)(pb) => [pc _] [pd _].
suff : x = class (prod_of_relation r r') (J (rep u) (rep v)).
  move => ->; apply: (class_class er'').
  by rewrite (substrate_prod_of_rel er er'); apply:setXp_i.
set_extens t.
  rewrite pe; move => /setX_P [qa qb qc].
  apply /(class_P er''); apply /prod_of_rel_P; aw.
  split; fprops; by apply :rel_in_class. 
move /(class_P er'') =>  /prod_of_rel_P; aw; move => [_ qa qb qc].
rewrite pe; apply /setX_P;split => //.
  apply: (rel_in_class2 er pa qb).
apply: (rel_in_class2 er' pb qc).
Qed.

Lemma ext_to_prod_rel_f r r':
  equivalence r -> equivalence r' ->
  function (ext_to_prod(canon_proj r)(canon_proj r')).
Proof. move=> er er'; apply: ext_to_prod_f; fprops. Qed.

Lemma ext_to_prod_rel_V r r' x x':
  equivalence r -> equivalence r' ->
  inc x (substrate r) -> inc x' (substrate r') ->
  Vf (ext_to_prod(canon_proj r)(canon_proj r'))  (J x x') =
  J (class r x) (class r' x').
Proof. 
move=> er er' xs xs'.  
rewrite ext_to_prod_V; fprops; aw.  
Qed.

Lemma compatible_ext_to_prod r r':
  equivalence r -> equivalence r' ->
   compatible_with_equiv (ext_to_prod (canon_proj r) (canon_proj r'))
     (prod_of_relation r r').
Proof. 
move=> er er'.
have fc: function (canon_proj r) by fprops.
have fc': function (canon_proj r') by fprops.
split; first by  apply: ext_to_prod_f. 
  by rewrite  substrate_prod_of_rel // /ext_to_prod; aw.
move=> x x'.
move /prod_of_rel_P=> [px px'].
move/(related_equiv_P er) => [pxs qx cx] /(related_equiv_P er') [pys qy cy].
have q1: (J (P x)(Q x) = x) by aw.
have q2: (J (P x')(Q x') = x') by aw.
rewrite -q1 ext_to_prod_V //; aw.  
rewrite  -q2 ext_to_prod_V //; aw. 
by rewrite cx cy.  
Qed.

Lemma compatible_ext_to_prod_inv r r' x x':
  equivalence r -> equivalence r' ->
  pairp x -> inc (P x) (substrate r) -> inc (Q x)  (substrate r') ->
  pairp x' -> inc (P x') (substrate r) -> inc (Q x')  (substrate r') ->
  Vf (ext_to_prod (canon_proj r) (canon_proj r')) x =
  Vf (ext_to_prod (canon_proj r) (canon_proj r')) x'
  -> related (prod_of_relation r r') x x'.
Proof. 
move=>  er er' px Px Qx px' Px' Qx'.
have p1: (J (P x) (Q x) = x) by aw. 
have p2: (J (P x') (Q x') = x') by aw. 
rewrite -p1 -p2 ext_to_prod_rel_V // ext_to_prod_rel_V // => Jeq.
move: (pr1_def Jeq) (pr2_def Jeq)=> eq1 eq2.
by apply/prod_of_rel_P; aw; split; fprops; apply/related_equiv_P.
Qed.

Lemma related_ext_to_prod_rel r r':
  equivalence r -> equivalence r' ->
  equivalence_associated (ext_to_prod(canon_proj r)(canon_proj r')) =
  prod_of_relation r r'.
Proof. 
move=> er er'.
move:(compatible_ext_to_prod er er')=> [fe se re].
have eq: equivalence (prod_of_relation r r')
   by apply: equivalence_prod_of_rel.
have eq' := proj1(graph_ea_equivalence fe). 
apply: sgraph_exten; fprops. 
have f1: function (canon_proj r) by fprops.
have f2: function (canon_proj r') by fprops. 
move=> u v; split.
  move /(ea_relatedP fe) => [].
  rewrite  {1 2} /ext_to_prod lf_source. 
  move /setX_P => [up Pu Qu] /setX_P [vp Pv Qv].
  have r1: (J (P u)(Q u) = u) by aw.
  have r2: (J (P v)(Q v) = v) by aw.
  rewrite  -r1 -r2 ext_to_prod_V // ext_to_prod_V //.
  move: Pu Qu Pv Qv; rewrite 2! canon_proj_s => Pu Qu Pv Qv.
  aw; move=> neq;  move: (pr1_def neq) (pr2_def neq)=> eq1 eq2.
  by apply /prod_of_rel_P;split; fprops; aw; apply/related_equiv_P.
move /prod_of_rel_P => [pu pv] /(related_equiv_P er)[Pu Pv c1]
    /(related_equiv_P er') [Qu Qv c2]. 
apply /(ea_relatedP fe); split.
  by rewrite /ext_to_prod lf_source; aw;apply/setX_P.
  by rewrite /ext_to_prod lf_source; aw;apply/setX_P.
by apply: re; apply/prod_of_rel_P; split => //; apply /(related_equiv_P).
Qed.

Lemma decomposable_ext_to_prod_rel r r':
  equivalence r -> equivalence r' ->
  exists h,  [/\ bijection h,
    source h = quotient (prod_of_relation r r'),
    target h = (quotient r) \times (quotient r') &
    h \co (canon_proj (prod_of_relation r r')) = 
    ext_to_prod(canon_proj r)(canon_proj r')].
Proof.
move=> er er'.
set (r'':=prod_of_relation r r').
set (f'':=ext_to_prod (canon_proj r) (canon_proj r')).
set (h:=fun_on_quotient r'' f'').
have er'': equivalence r'' by rewrite /r''; apply: equivalence_prod_of_rel. 
have co: compatible_with_equiv f'' r''.
  rewrite /f'' /r'';  apply: compatible_ext_to_prod=>//. 
move :(compose_foq_proj er'' co); rewrite -/h => cop.
have sh: source h = quotient r''.
   by rewrite /h /fun_on_quotient/section_canon_proj; aw.
have th: target h = (quotient r) \times (quotient r').
  rewrite /h/fun_on_quotient/ f'' /ext_to_prod; aw.
have fh: function h.
  rewrite /h /f''; apply: foqc_f =>//.
    apply: ext_to_prod_f; fprops. 
  by rewrite /r'' substrate_prod_of_rel // /ext_to_prod; aw.
have ff'': function f'' by rewrite /f''; apply: ext_to_prod_rel_f.
have sf'':  source f'' = substrate r''. 
  rewrite /f'' /r''/ext_to_prod substrate_prod_of_rel; aw. 
have ih: injection h.
  split=>//. 
  move=> x y; rewrite sh /h => xs ys.  
  rewrite foqc_V // foqc_V //.
  move: (rep_i_sr er'' xs)(rep_i_sr er'' ys). 
  rewrite substrate_prod_of_rel //.
  move=> /setX_P [px Px Qx] /setX_P [py Py Qy] WW.
  move: (compatible_ext_to_prod_inv er er' px Px Qx py Py Qy WW).
  by move/(related_rr_P er'' xs ys). 
exists h;split => //;split =>//;split =>//.
move=> y; rewrite th; move /setX_P=> [py Py Qy].
have p1: (inc (J (rep (P y)) (rep (Q y))) (substrate r'')).
  rewrite /r'' substrate_prod_of_rel //;apply:setXp_i; fprops.
set (x:= class r'' (J (rep (P y)) (rep (Q y)))).
have xq: inc x (quotient r'') by rewrite /x; fprops.
have rxs: inc (rep x) (substrate r'') by fprops.
move: (related_rep_class er'' p1).
move: rxs; rewrite substrate_prod_of_rel;aw;move /setX_P => [ pr Pr Qr].
move: p1; rewrite substrate_prod_of_rel; aw; move /setXp_P=>  [Py' Qy'].
rewrite -/x; move /(related_prod_of_relP1)=> [u [v [e1 e2 e3]]].
exists x; rewrite ?sh // /h foqc_V //- pr - py /f'' ext_to_prod_rel_V //. 
have <-: (P y = class r (P (rep x))). 
  apply: is_class_pr =>//; rewrite e1; aw.
  by move:Py => /(setQ_P er) [_ ->]; apply /(class_P er).
have <- //: (Q y = class r' (Q (rep x))) . 
  apply: is_class_pr =>//; rewrite e1; aw.
  by move:Qy => /(setQ_P er') [_ ->]; apply /(class_P er').
Qed.


Section LeastEquiv.

Definition eqv_smaller (R: relation) r :=
  forall x y, R x y -> related r x y.     

Definition eqv_smallest E R :=
  intersection (Zo (equivalences E) (eqv_smaller R)).

Lemma eqv_smallest_prop E R (r := (eqv_smallest E R)):
  (forall x y, R x y -> inc x E /\ inc y E) ->
  equivalence_on r E /\ eqv_smaller R r.
Proof.
move => ha.
have hb:equivalence r.
  apply: setIrel_equivalence.
  by move => t /Zo_P [/equivalencesP []].
have ne:nonempty (Zo (equivalences E) (eqv_smaller R)).
  exists (coarse E); apply/Zo_P; split.
    apply: inc_coarse_all_equivalence_relations.
  by move => x y /ha /coarse_related.
have sr: substrate r = E.
  by apply:(setIrel_sr ne) => t /Zo_P [/equivalencesP []] // [].
split => //  x y rxy.
by apply/(setI_P ne) => s /Zo_P [uu]; apply.
Qed.

Lemma eqv_smallest_prop2 E (R: relation) r:
  (forall x y, R x y -> inc x E /\ inc y E) ->
  equivalence_on r E -> eqv_smaller R r ->
  (forall r', equivalence_on r' E -> eqv_smaller R r' -> sub r r') ->
  r = eqv_smallest E R.
Proof.
move => ep er sm h.
set F := (Zo (equivalences E) (eqv_smaller R)).
have ha: inc r F by apply/Zo_P; split => //; apply/equivalencesP.
move:(eqv_smallest_prop ep) => [hb hc]; move:(h _ hb hc) => sub1.
by apply: extensionality => //; apply:setI_s1.
Qed.

Lemma eqv_smallest_sym E (R: relation):
  (forall x y, R x y -> inc x E /\ inc y E) ->
  (eqv_smallest E R) = (eqv_smallest E (fun x y => R x y \/ R y x)).
Proof.
move => ha.
set R' := (fun x y : Set => R x y \/ R y x).
rewrite /eqv_smallest.
congr intersection; apply: Zo_exten1 => s /equivalencesP[eq ss].
split => h x y.
    case; [ by apply:h | move/h ; apply:(proj44 eq)].
by move=> rxy; apply:h; left.
Qed.

Lemma eqv_smallest_refl E (R: relation)
      (R' :=  fun x y => R x y \/ (inc x E /\ x = y)):
  (forall x y, R x y -> inc x E /\ inc y E) ->
  (eqv_smallest E R) = (eqv_smallest E  R').
Proof.
move => ha.
rewrite /eqv_smallest.
congr intersection; apply: Zo_exten1 => s /equivalencesP[eq ss].
split => h x y.
  case; [ by apply: h | by move => [xE <-];  apply:(proj42 eq); rewrite ss ].
by move=> rxy; apply:h; left.
Qed.


(** A chain is a list with at least two elements; it has a head and a tail. *)

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 concat_chain x y : chain :=
  match x with chain_pair u _ => chain_next u y 
| chain_next u v => chain_next u  (concat_chain v y) end.

Lemma head_concat x y:
  chain_head (concat_chain x y) = chain_head x.
Proof. by case: x.  Qed.

Lemma tail_concat x y: 
  chain_tail (concat_chain x y) = chain_tail y.
Proof. by elim: x. Qed.



(** We may revert a chain *)
Fixpoint reconc_chain (x y:chain)  :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 x y: chain_tail (reconc_chain x y) = chain_tail y.
Proof.  by move: x y; elim=> [a b y | a c r] // y; by rewrite r. Qed.

Lemma head_reconc x y:chain_head (reconc_chain x y) = chain_tail x.
Proof. move: x y; elim=> [a b y | a c r] // y; by rewrite r. 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 x: chain_head (chain_reverse x) = chain_tail x.
Proof. elim x=>// y;elim =>// P c h h1 /=; apply: head_reconc.
Qed.

Lemma tail_reverse x: chain_tail (chain_reverse x) = chain_head x.
Proof. elim: x =>// y;elim =>// P c h h1 /=; apply: tail_reconc. Qed.



Variables (R:relation) (E:Set).
Hypotheses (A1: reflexive_re R E)(A2: symmetric_r R)
  (A3: forall x y, R x y -> inc x E).


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.


Lemma chained_concat x y:
  chained_r x -> chained_r y -> chain_tail x = chain_head y ->
  chained_r (concat_chain x y).
Proof. 
move=> cx cy txhy;elim: x cx txhy => [a b cp ct| a c r cp ct].
  split=>//; by  rewrite -ct //.
by move: cp => [pa pb];split; [rewrite head_concat | apply: r].
Qed.

Lemma chained_reconc x y: chained_r x -> chained_r y -> 
  R (chain_head y) (chain_head x) ->  chained_r (reconc_chain x y).
Proof. 
move: x y; elim => [a b y c cy | P c r]=>//=; auto.
by move=> y [rPh cc] cy RhyP; apply: r=>//; split => //; apply: A2.
Qed.


Lemma chained_reverse x: chained_r x -> chained_r (chain_reverse x).
Proof. 
elim: x; first by move=> a b;apply:A2.
move=> a; elim; first by move => b c /= _ [/A2 h2 /A2 h3]. 
move=> b c hr hr1 /= [/A2 Rab [Rbc cc]].
by apply: chained_reconc. 
Qed.

Definition chain_related x y := exists c:chain, 
  [/\ chained_r c, chain_head c = x  & chain_tail c = y].

Definition chain_equivalence := graph_on chain_related E.

Lemma chain_related_re x:
  inc x E <-> chain_related x x.
Proof.
split.
  by move=> xE; exists (chain_pair x x);split => //;  apply /A1.
case; case => a b [h <- _]; [by  apply: (A3 h) | by  case:h => /A3 ].
Qed.
  
Lemma chain_equivalence_eq: equivalence_on chain_equivalence E.
Proof.
split; last by apply: graph_on_sr => x /chain_related_re.
apply: equivalence_from_rel.
split.
  move=> x y [c [cc hcx tcy]].
  exists (chain_reverse c); split.
  + by apply: chained_reverse.
  + by rewrite head_reverse.
  + by rewrite tail_reverse.
move => y x z [c [cc hcx tcy]][c' [cc' hcy  tcz]].
exists (concat_chain c c'); split => //.
    apply: chained_concat=>//;  ue. 
  by rewrite head_concat.
by rewrite tail_concat.
Qed.


Lemma chain_equivalence_is_smallest:
  chain_equivalence = eqv_smallest E R.
Proof.
apply:eqv_smallest_prop2.
+ move => x y rxy;split; [exact: (A3 rxy)| exact (A3 (A2 rxy))].
+ exact chain_equivalence_eq.
+  move => x y Rxy;apply/graph_on_P1; split.
   - apply: (A3 Rxy).
   - apply: (A3 (A2 Rxy)).
   - exists (chain_pair x y); split => //.
+ move => r' [er' _] p q. 
  have aux:(forall w, chained_r w -> inc (J (chain_head w) (chain_tail w)) r').
    elim => [a b | a c h [aux cc]] //=; first by apply: p.
    move: (h cc)(p _ _ aux) => r1 r2; apply:(proj43 er' _ _ _ r2 r1).
  move /Zo_P => [pp  [c [cc hcx htx]]].
  have <-: (J (P q)(Q q) = q) by move/setX_P: pp => [pp _].
  by rewrite -hcx -htx ; apply: aux.
Qed.

End LeastEquiv.

End Relation.
Export Relation.