proposition: Lemma substrate_union_diag x g: sub g (coarse x) -> substrate (g \cup (diagonal x)) = x.
proof: Proof. move=> gc. have gg: sgraph g by move=> t tg; move: (gc _ tg) => /setX_P []. have gu: sgraph (g \cup (diagonal x)). by move=> t; case /setU2_P; [ auto | move/diagonal_i_P => []]. set_extens y. case /(substrate_P gu) => [] [z] /setU2_P []. - by move => h; move: (gc _ h); move /setXp_P=> []. - by move/diagonal_pi_P => []. - by move => h; move: (gc _ h); move /setXp_P=> []. - by move/diagonal_pi_P => [ h <-]. move=> yx. have aux: inc (J y y) (g \cup (diagonal x)). by apply: setU2_2; apply /diagonal_pi_P; split. substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)