proposition: Lemma kconnected_degree (G : sgraph) k (x : G) : k.-connected G -> k <= #|N(x)|.
proof: Proof. move => [card_G sep_G]. case: (boolP [exists (y | x != y), ~~ x -- y]). - case/exists_inP => y xDy xNy. by apply/sep_G/separates_vseparator; apply: opn_separates xNy. - rewrite negb_exists_in => /forall_inP; setoid_rewrite negbK => Hx. apply: (@leq_trans #|[set~ x]|). + by rewrite cardsC1 -ltnS (@ltn_predK k). + apply/subset_leq_card/subsetP => x'. rewrite !inE eq_sym. exact: Hx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)