proposition: Theorem edges_sum_degrees (G : sgraph) : 2 * #|E(G)| = \sum_(x in G) #|N(x)|.
proof: Proof. elim/(size_ind (fun G => #|E(G)|)) : G => G IH. case: (set_0Vmem E(G)) => [E0|[e edge_e]]. - rewrite E0 cards0 muln0. under eq_bigr => x do rewrite edges_opn0 //. by rewrite sum_nat_const muln0. - have [x [y] [def_e xy]] := edgesP _ edge_e; set G' := del_edges e. have/IH E' : #|E(G')| < #|E(G)|. { by apply: proper_card; exact: del_edges_proper edge_e _. } rewrite (del_edges1 edge_e) cardsU1 del_edgesN mulnDr /= muln1 {}E' /=. rewrite [in LHS](bigID (mem e)) [in RHS](bigID (mem e)) /= addnA. congr (_ + _); last first. { apply eq_bigr => z zNe; apply eq_card => w. by rewrite del_edges_opn subUset sub1set (negbTE zNe) /= andbT. } rewrite def_e !big_setU1 ?inE ?sg_edgeNeq //= !big_set1. suff Ne w : w \in e -> #|N(G';w)|.+1 = #|N(G;w)|. { rewrite -!Ne ?def_e ?in_set2 ?eqxx ?orbT //. by rewrite [RHS]addSn [in RHS]addnS add2n. } rewrite {}/G' {}def_e => {edge_e} w_in_xy. wlog w_is_x : x y xy {w_in_xy} / w = x. { move => W. case/set2P : w_in_xy; first exact: W. by rewrite setUC; apply: W; rewrite sgP. } subst w; suff -> : N(G;x) = y |: N(del_edges [set x;y];x). { by rewrite cardsU1 del_edges_opn subxx andbF add1n. } apply/setP => z; rewrite 2!inE del_edges_opn !inE. rewrite subUset subsetUl sub1set !inE /=. case: (eqVneq z y) => [-> //|zDy /=]. case: (eqVneq z x) => [->|]; by rewrite ?sg_irrefl //= ?orbT ?andbT. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)