proposition: Lemma konnected_del1 k (G : sgraph) (x : G) : k.+1.-connected G -> k.-connected (induced [set~ x]).
proof: Proof. by move => kG; apply: kconnected_induced; rewrite setCK cards1 addn1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)