proposition: Lemma mono_path_in x s : {in P &, {mono f : x y / e x y >-> e' x y}} -> all P (x :: s) -> path e' (f x) (map f s) = path e x s.
proof: Proof. by move=> f_mono; rewrite path_map; apply: eq_in_path. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)