proposition: Lemma has_edge (G : graph) (x y : G) : connected [set: skeleton G] -> x != y -> 0 < #|edge G|.
proof: Proof. move/connectedTE/(_ x y). case/connect_irredP => p _ xy. case: (splitL p xy) => x' [/= xx'] _. apply/card_gt0P. case/andP: xx' => _. case/existsP=> e _. by exists e. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)