proposition: 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: 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). by 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 rewrite canon_proj_V // cx; apply: class_eq1. by Wtac; aw. move/dirim_P => [y ya Jg]; move: (sa _ ya)=> yu. move: (Vf_pr fc Jg); rewrite canon_proj_V // => 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) => [_ _]. by rewrite -/z; Wtac; rewrite/f/fun_on_quotients/section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)