proposition: Lemma sub_Kn n (G : sgraph) : #|G| <= n -> subgraph G 'K_n.
proof: Proof. move=> leGn; pose h (x : G) : 'K_n := widen_ord leGn (enum_rank x). by exists h; move => // x y /(congr1 val) E; apply /enum_rank_inj/ord_inj. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)