proposition: Lemma exists_unique_fun_on_quotient f r h: equivalence r -> compatible_with_equiv f r -> h \coP (canon_proj r) -> h \co (canon_proj r) = f -> h = fun_on_quotient r f.
proof: Proof. move=> er cfr chc chcf; move: (cfr) => [ff sf1 _]. have sc: (surjection (canon_proj r)) by apply: canon_proj_fs. have ri := (right_inv_canon_proj er). have sf: source f = source (canon_proj r) by aw. apply: (exists_left_composable_aux ff sf ri chc chcf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)