proposition: Lemma mono_path x s : {mono f : x y / e x y >-> e' x y} -> path e' (f x) (map f s) = path e x s.
proof: Proof. by move=> f_mon; rewrite path_map; apply: eq_path. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)