proposition: Lemma path_closed (A : pred G) x y (p : Path x y) : x \in A -> (forall y z, y \in A -> y -- z -> z \in A) -> {subset p <= A}.
proof: Proof. move => xA clos_A. move: xA. pattern x,y,p. apply: Path_ind => {x p}. - move => yA z. by rewrite mem_idp => /eqP->. - move => x z p xz IH xA u. rewrite mem_pcat mem_edgep -orbA. have ? : z \in A by exact: clos_A xz. case/or3P => [/eqP->|/eqP->|] //. exact: IH. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)