proposition: Lemma finer_sub_equivP2: (finer_equivalence s r <-> (forall x, exists y, sub (class s x) (class r y))).
proof: Proof. move: fa=> [es er srss]. split. move=> fsr x; exists x. by move=> u /(class_P es) h; apply /(class_P er); apply:fsr. move=> h x y rxy. move:(h x)=> [z sxz]. have xs: inc x (substrate s) by substr_tac. have ixc: inc x (class s x) by fprops. have ys: inc y (class s x) by apply /(class_P es). move: (sxz _ ixc)(sxz _ ys) => /(class_P er) pa /(class_P er) pb; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)