proposition: Lemma connectRI (A : pred D) x y (p : Path x y) : {subset p <= A} -> connect (restrict A (--)) x y.
proof: Proof. case: (boolP (x == y)) => [/eqP ?|]; first by subst y; rewrite connect0. move => xy subA. apply/connect_irredRP => //. case: (uncycle p) => p' p1 p2. exists p' => //. apply/subsetP => z /p1. exact: subA. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)