proposition: Lemma composable_fun_proj r f b: equivalence r -> lf_axiom f (substrate r) b -> (function_on_quotient r f b) \coP (canon_proj r).
proof: Proof. move=> er ta. by split; [apply: foq_f | fprops | rewrite/function_on_quotient; aw ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)