proposition: Lemma exists_fun_on_quotient f r: equivalence r -> function f -> source f = substrate r -> (compatible_with_equiv f r <-> (exists h, h \coP (canon_proj r) /\ h \co (canon_proj r) = f)).
proof: Proof. move=> er ff sf. rewrite exists_left_composable; aw => //; last by apply: canon_proj_fs. split. by move => co x y xs ys sW; apply: (compatible_with_proj er co xs ys sW). move=> hyp; split=>//. move=> x x' /(related_equiv_P er) [xs ys cc];apply: hyp => //. by rewrite ! canon_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)