proposition: Lemma composable_fun_projcs r r' f: equivalence r -> equivalence r' -> compatible_with_equivs f r r'-> (fun_on_quotients r r' f) \coP (canon_proj r).
proof: Proof. move=> er er' [ff sf [fg sg h]]. move: sg; aw => sg. split; fprops;first by apply: foqcs_f. by rewrite/fun_on_quotients/section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)