proposition: Lemma saturatedP r x: equivalence r -> sub x (substrate r) -> ((saturated r x) <-> (forall y, inc y x -> sub (class r y) x)).
proof: Proof. move=> er sxs; split. move=> sr y yx t; move/(class_P er); apply: (sr _ _ yx). by move=> yw u v ux ruv; apply: (yw _ ux); apply/(class_P er). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)