proposition: Lemma add_edge_avoid (G : sgraph) (s1 s2 x y : G) (p : @Path (add_edge s1 s2) x y) : (s1 \notin p) || (s2 \notin p) -> exists q : @Path G x y, nodes q = nodes p.
proof: Proof. move => H. wlog H : s1 s2 p {H} / s1 \notin p => [W|]. { case/orP: H => [|Hs]; first exact: W. case: (add_edge_pathC p) => p' Hp'. case: (W _ _ p' _). by rewrite (mem_path p') Hp' -(mem_path p). move => q Hq. exists q. congruence. } have pP u : u \in p -> u == s1 = false. { by apply: contraTF => /eqP->. } case: (@lift_Path_on G (add_edge s1 s2) id x y p) => //. - move => u v up vp /=. by rewrite {1}/edge_rel/= !(pP u,pP v) //= !andbF !orbF. - 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)