proposition: Lemma coarse_equivalence u: equivalence_on (coarse u) u.
proof: Proof. have sr: substrate (coarse u) = u. rewrite /coarse/substrate. transitivity (u \cup u); last by apply: setU2_id. case: (emptyset_dichot u); first by move ->; rewrite setX_0l; aw. by move=> h; aw;rewrite setX_domain // setX_range //. split; [split | exact]. - by apply: coarse_graph. - by move => y; rewrite sr => yu;apply/ coarse_related. move=> x y z /coarse_related [pa pb]/coarse_related [pc pd]. - by apply/coarse_related. - by move=> x y /coarse_related [pc pd]; apply/coarse_related. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)