proposition: Lemma connect_restrict_case x y (A : pred D) : connect (restrict A (--)) x y -> x = y \/ [/\ x != y, x \in A, y \in A & connect (restrict A (--)) x y].
proof: Proof. case: (altP (x =P y)) => [|? conn]; first by left. case/connect_irredRP : (conn) => // p _ /subsetP subA. right; split => //; by rewrite subA ?path_end ?path_begin. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)