proposition: Lemma compose_foq_proj f r: equivalence r -> compatible_with_equiv f r -> (fun_on_quotient r f) \co (canon_proj r) = f.
proof: Proof. move=> er co; move: (co)=> [ff sf hyp]. set (g:= canon_proj r). have sg: surjection g by rewrite/g; apply: canon_proj_fs. have sfsg: source f = source g by rewrite /g; aw. have sW: forall x y, inc x (source g) -> inc y (source g) -> Vf g x = Vf g y -> Vf f x = Vf f y. rewrite - sfsg sf; move=> x y xr yr h. by apply: (compatible_with_proj er co xr yr). apply: (left_composable_value ff sg sfsg sW (right_inv_canon_proj er) (refl_equal (fun_on_quotient r f))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)