proposition: Lemma add_edge_pathC (G : sgraph) (s1 s2 x y : G) (p : @Path (add_edge s1 s2) x y) : exists q : @Path (add_edge s2 s1) x y, nodes q = nodes p.
proof: Proof. case: (@lift_Path (add_edge s2 s1) (add_edge s1 s2) id x y p) => //. - move => u v. by rewrite add_edgeC. - move => u. by rewrite mem_map // mem_enum. - move => q Hq _. exists q. by rewrite -Hq map_id. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)