proposition: Lemma foq_finer_f: finer_equivalence s r -> function(fun_on_quotient s (canon_proj r)).
proof: Proof. by move : fa=> [es er fh] fe; apply: foqc_f; fprops; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)