proposition: Lemma sub_graph_coarse_substrate r: sgraph r -> sub r (coarse (substrate r)).
proof: Proof. rewrite /coarse=> gr t tr; apply: setX_i; first (by apply: gr); substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)