proposition: Lemma fun_on_quotient_pr5 r r' f x: equivalence r -> equivalence r' -> compatible_with_equivs f r r'-> inc x (substrate r) -> Vf (canon_proj r') (Vf f x) = Vf (fun_on_quotients r r' f) (Vf (canon_proj r) x).
proof: Proof. move => er er' co xs. move: (co)=> [ff sf [fg sg h]]; move: sg; rewrite compf_s => sg. have cc: composable (canon_proj r') f by split; fprops;symmetry; aw. rewrite - compfV //; try ue. rewrite - compfV //; last by aw. by rewrite -fun_on_quotient_pr4 //. by apply: composable_fun_projcs=>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)