proposition: Lemma finer_sub_equivP3: (finer_equivalence s r <-> forall y, saturated s (class r y)).
proof: Proof. move: (fa)=>[es er srss]. split. move=> fe y. apply/(saturatedP es); first by rewrite - srss; apply: sub_class_substrate. move => z zc; move: fe => /finer_sub_equivP2 fe. move/(class_P er): (zc) => r1. have zs: (inc z (substrate s)) by rewrite - srss; substr_tac. move: (fe z)=> [x cxy]. suff: (class r x = class r y) by move=> <-. have: (inc z (class r x)) by apply: cxy; fprops. move => /(class_P er) r2. apply: (class_eq1 er); equiv_tac. move=> p x y re; move: (p x). move: (sub_class_substrate er (x:=x)); rewrite srss => aux. move /(saturatedP es aux) => h. have p1: inc x (substrate s) by substr_tac. have p2: inc x (class r x) by rewrite - srss in p1;fprops. have p3: inc y (class s x) by apply/class_P. by move:((h _ p2) _ p3) => /(class_P er). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)