proposition: Lemma diso_replicate (G : sgraph) (v : G) : G ≃ @induced (replicate v) [set~ None].
proof: Proof. exact: diso_add_nodeK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)