proposition: Lemma Knm_edges n m : E('K_n,m) = [set [set inl x; inr y] | x in [set:'I_n], y in [set: 'I_m]].
proof: Proof. apply/setP=> e. apply/edgesP/imset2P => [|[x y _ _ ->]]; last by exists (inl x), (inr y). by move=> [[x|x] [[y|y] [// -> _]]]; [exists x y|exists y x]; rewrite // setUC. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)