proposition: Lemma lift_Path_on (G H : sgraph) (f : G -> H) a b (p' : Path (f a) (f b)) : (forall x y, f x \in p' -> f y \in p' -> f x -- f y -> x -- y) -> injective f -> {subset p' <= codom f} -> exists2 p : Path a b, map f (nodes p) = nodes p' & irred p = irred p'.
proof: Proof. move => A I S. case: (lift_pathp_on _ I (valP p') _). - move => x y. rewrite -!nodesE -!mem_path. exact: A. - move => x V. apply: S. by rewrite mem_path nodesE inE V. - move => p [p1 p2]. exists (Sub p p1). + by rewrite !nodesE /= p2. + by rewrite !irredE !nodesE -p2 -map_cons map_inj_uniq. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)