proposition: Lemma add_node_lift_Path (x y : G) (p : Path x y) : exists q : @Path add_node (Some x) (Some y), nodes q = map Some (nodes p).
proof: Proof. case: p => p0 p'. set q0 : seq add_node := map Some p0. have q' : @pathp add_node (Some x) (Some y) q0. move: p'; rewrite /pathp/= last_map (inj_eq (@Some_inj _)). move=> /andP[p' ->]; rewrite andbT. exact: homo_path p'. by exists (Sub _ q'); rewrite !nodesE /=. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)