proposition: Lemma diso_Kn (G : sgraph) : (forall x y : G, x != y -> x -- y) -> diso G 'K_#|G|.
proof: Proof. move => completeG; apply: (@Diso G 'K_#|G| bij_ord). - by move=> x y xy; rewrite /edge_rel/= -(inj_eq enum_val_inj) !enum_rankK sg_edgeNeq. - move => x y xy /=. apply: completeG. by rewrite -(inj_eq enum_rank_inj) !enum_valK. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)