proposition: Lemma kconnected_complete G k : k.-connected G -> #|G| <= k.+1 -> (forall x y : G, x != y -> x -- y).
proof: Proof. move => [lt_k_G sepG] le_G_k x y xDy; pose S := [set~ x] :&: [set~ y]. apply: contraTT le_G_k => xNy; rewrite -ltnNge. have/sepG le_k_S : vseparator S. by apply/proper_vseparator/separate_nonadjacent. by rewrite -(cardsC S) setCI !setCK cards2 xDy /= addn2. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)