proposition: Lemma card_edge_Knm n m : #|E('K_n,m)| = n * m.
proof: Proof. rewrite Knm_edges curry_imset2X card_imset ?cardsX ?cardsT ?card_ord //=. by move => [x y] [x' y']; rewrite /= doubleton_eq_iff => -[[[->] [->]]|[//]]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)