proposition: Lemma compatible_with_proj f r x y: equivalence r -> compatible_with_equiv f r -> inc x (substrate r) -> inc y (substrate r) -> Vf (canon_proj r) x = Vf (canon_proj r) y -> Vf f x = Vf f y.
proof: Proof. move=> er cgt xs ys; rewrite !canon_proj_V // => sx. apply: (@compatible_constant_on_classes _ r) =>//; rewrite sx; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)