proposition: Lemma sum_cardI (T : finType) (A B : {set T}): \sum_(x in A) (x \in B) = #|A :&: B|.
proof: Proof. rewrite -sum1_card; under [RHS]eq_bigl do rewrite inE. by rewrite [RHS]big_mkcondr /=; apply: eq_bigr => i _; case: (_ \in _). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)