proposition: Lemma foqcs_V r r' f x: equivalence r -> equivalence r' -> function f -> source f = substrate r -> target f = substrate r' -> inc x (quotient r) -> Vf (fun_on_quotients r r' f) x = class r' (Vf f (rep x)).
proof: Proof. move=> er er' ff sf tf xq. rewrite /fun_on_quotients. have fs: function(section_canon_proj r) by apply: section_canon_proj_f. have ccf: (canon_proj r') \coP f by split; fprops; symmetry;aw. have cc2: ( (canon_proj r') \co f) \coP (section_canon_proj r). by split; first (by fct_tac); rewrite /section_canon_proj; aw. have Wt: inc (Vf (section_canon_proj r) x) (target (section_canon_proj r)). by Wtac; rewrite /section_canon_proj; aw. have irs: inc (rep x) (source f) by ue. rewrite compfV //; last by rewrite/section_canon_proj; aw. rewrite section_canon_proj_V // compfV // canon_proj_V //; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)