proposition: Lemma compatible_with_pr r r' f x y: equivalence r -> equivalence r' -> compatible_with_equivs f r r' -> related r x y -> related r' (Vf f x) (Vf f y).
proof: Proof. move=> er er' [ff sf [fc sc hyp]] rxy. have cc: ((canon_proj r') \coP f) by split; first (by fprops); aw. move: sc; aw => sc. have xs: inc x (source f) by rewrite sc; substr_tac. have ys: inc y (source f) by rewrite sc; substr_tac. have px: (inc (Vf f x) (substrate r')) by Wtac. have py: (inc (Vf f y) (substrate r')) by Wtac. move: (hyp _ _ rxy). rewrite ! compfV // !canon_proj_V // => sc1. by apply/related_equiv_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)