proposition: Lemma fun_on_quotient_pr4 r r' f: equivalence r -> equivalence r' -> compatible_with_equivs f r r'-> (canon_proj r') \co f = (fun_on_quotients r r' f) \co (canon_proj r).
proof: Proof. rewrite/fun_on_quotients; move=> er er' [ff sf h]. symmetry; apply: (compose_foq_proj er h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)