proposition: 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: 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; trivial;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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)