proposition: Lemma compatible_with_proj3 r r' f x y: equivalence r -> equivalence r' -> compatible_with_equivs f r r'-> inc x (substrate r) -> inc y (substrate r) -> Vf (canon_proj r) x = Vf (canon_proj r) y -> class r' (Vf f x) = class r' (Vf f y).
proof: Proof. move=> er er' co xs ys; rewrite !canon_proj_V // => sc. apply: class_eq1 =>//; apply: (compatible_with_pr er er' co). by apply /(related_equiv_P er). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)