proposition: Lemma add_edge_Path (G : sgraph) (i o x y : G) (p : @Path G x y) : exists q : @Path (add_edge i o) x y, nodes q = nodes p.
proof: Proof. case: p => p p_pth. have p_iopth : @pathp (add_edge i o) x y p. { case/andP: p_pth => p_path p_last. apply/andP; split=> //. apply: sub_path p_path. rewrite {2}/edge_rel/=. by move=> u v /=->. } by exists (Sub (p : seq (add_edge i o)) p_iopth). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)