proposition: Lemma ea_foq_on_im_fb f: function f -> bijection (restriction2 (fun_on_quotient (equivalence_associated f) f) (quotient (equivalence_associated f)) (Imf f)).
proof: 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: Imf f = Vfs h (quotient g). rewrite rg qg restriction1_pr //. apply: restriction1_fb; fprops. set_extens t. move /(Imf_P 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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)