proposition: Lemma diso_add_nodeK (G : sgraph) (A : {set G}) : G ≃ @induced (add_node G A) [set~ None].
proof: Proof. set H := induced _. have h_proof (x : G) : Some x \in [set~ None] by rewrite !inE. pose h (x : G) : H := Sub (Some x) (h_proof x). have default (x : H) : G by case: x => -[x//|]; rewrite !inE eqxx. pose g (x : H) : G := if val x is Some z then z else default x. have can_h : cancel h g by []. have can_g : cancel g h. move => [[x|] p]; [exact: val_inj|by exfalso; rewrite !inE eqxx in p]. exact: Diso' can_h can_g _. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)