proposition: Lemma composable_fun_projc r f: equivalence r -> compatible_with_equiv f r -> (fun_on_quotient r f) \coP (canon_proj r).
proof: Proof. move=> er [ff sf h]. split; [ by apply: foqc_f | fprops | ]. by rewrite/fun_on_quotient/section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)