proposition: Lemma card_edge_add_node (G : sgraph) (A : {set G}) : #|E(add_node G A)| = #|A| + #|E(G)|.
proof: Proof. rewrite edges_add_node cardsU disjoint_setI0 ?cards0 ?subn0; first congr (_ + _). - apply: card_imset => x y /setP /(_ (Some y)); rewrite !inE eqxx orbT. by rewrite Some_eqE => /eqP ->. - apply: card_imset => e1 e2 eq_Some; apply/setP => x. by rewrite -[LHS](mem_imset _ _ Some_inj) eq_Some mem_imset. - apply/disjointP => e E1 E2. have: None \in e by case/imsetP : E1 => x _ ->; rewrite !inE eqxx. suff: None \notin e by move/negPf->. by case/imsetP : E2 => x _ ->; apply/negP=>/imsetP => -[?]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)