proposition: Lemma card_edge_Kn n : #|E('K_n)| = 'C(n,2).
proof: Proof. rewrite -[in RHS](card_ord n) -card_draws; apply: eq_card => e. by rewrite !inE; apply/edgesP/cards2P => [[x[y[-> xy]]]|[x[y[xy ->]]]]; exists x,y. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)