proposition: Lemma compatible_constant_on_classes f r x y: equivalence r -> compatible_with_equiv f r -> inc y (class r x) -> Vf f x = Vf f y.
proof: Proof. by move=> eq [ff sf hyp] yc; apply: hyp; move/(class_P eq): yc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)