proposition: Lemma sub_coarse g: equivalence g -> sub g (coarse (substrate g)).
proof: Proof. move=> eg; move: (sub_graph_setX (proj41 eg)). by rewrite range_is_substrate // domain_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)