proposition: Lemma path_rpath (T : eqType) (e : rel T) (A : pred T) x p : path e x p -> x \in A -> {subset p <= A} -> path (restrict A e) x p.
proof: Proof. elim: p x => [//|a p IH] x /= /andP[-> pth_p] -> /cons_subset [Ha ?] /=. rewrite /= Ha. exact: IH. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)