proposition: Lemma diso_add_edge_KSn n : diso 'K_n.+1 (add_node 'K_n setT).
proof: Proof. set G := add_node _ _; apply: diso_sym. have -> : n.+1 = #|G| by rewrite card_option card_ord. by apply: diso_Kn => -[x|] [y|] // _; rewrite /edge_rel/= inE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)