proposition: Lemma compatible_with_pr2 r r' f: equivalence r -> equivalence r' -> function f -> target f = substrate r'-> source f = substrate r-> (forall x y, related r x y -> related r' (Vf f x) (Vf f y)) -> compatible_with_equivs f r r'.
proof: Proof. move=> er er' ff tf sf rr'. have cc: (canon_proj r') \coP f by split; fprops; symmetry; aw. split =>//; saw;first by fct_tac. move=> x x' rxx'; move: (rr' _ _ rxx'); move /(related_equiv_P er'). move => [Ws Ws' cxx']. rewrite ! compfV // ? canon_proj_V // sf; substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)