proposition: Lemma ea_foq_fi f: function f -> injection (fun_on_quotient (equivalence_associated f) f).
proof: 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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)