proposition: Lemma closed_path_sub (T : eqType) (e : rel T) (x : T) (s : seq T) (p : {pred T}) : (forall z y, e z y -> p z -> p y) -> p x -> path e x s -> {subset s <= p}.
proof: Proof. move => cl_p; elim: s x => //= y s IHs x /cl_p py /andP[e_xy pth_p]. apply/all_cons; split; by [apply: py |apply: IHs (py _ _) pth_p]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)