proposition: Lemma rpath_sub (T : eqType) (e : rel T) (a : pred T) x p : path (restrict a e) x p -> {subset p <= a}.
proof: Proof. elim: p x => //= b p IH x. rewrite -!andbA => /and4P[H1 H2 H3 H4]. apply/cons_subset. by split; eauto. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)