proposition: Lemma lift_Path (G H : sgraph) (f : G -> H) a b (p' : Path (f a) (f b)) : (forall x y, 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 => ?. apply: lift_Path_on; auto. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)