proposition: Lemma foq_finer_fs: finer_equivalence s r -> surjection(fun_on_quotient s (canon_proj r)).
proof: 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 /(class_P es);apply: rep_i; rewrite /x. apply /(setQ_ne es); apply /(setQ_P es); apply/(class_class es); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)