proposition: Lemma del_edge_path_case (x y : G) (p : Path x y) (Ip : irred p) : (exists (p1 : @IPath del_edge x a) (p2 : @IPath del_edge b y), [/\ nodes p = nodes p1 ++ nodes p2, a \notin p2 & b \notin p1]) \/ (exists p1 : @IPath del_edge x y, nodes p = nodes p1).
proof: Proof. pattern x, y, p. apply irred_ind => //. - move => {p Ip}. have Ip : irred (@idp del_edge y) by apply: irred_idp. by right;exists (Sub _ Ip). - move => {x p Ip} x z p xz Ip xp [[p1] [p2] [A B C]|[p1] E]. + left. have xyD : (x:del_edge) -- z. { rewrite /edge_rel/= xz (_ : x != a) //. apply: contraNneq xp => -> . by rewrite mem_path A mem_cat -(@mem_path del_edge) path_end. } have Iq : irred (pcat (edgep xyD) p1). { rewrite irred_edgeL (valP p1) andbT. rewrite mem_path A mem_cat -(@mem_path del_edge) negb_or in xp. by case/andP : xp. } exists (Sub _ Iq). exists p2. split => //. * by rewrite /= !nodes_pcat A [nodes p1](nodesE) /= -catA. * change (b \notin pcat (edgep xyD) p1). rewrite (@mem_pcat del_edge) (negbTE C) orbF mem_edgep negb_or. rewrite irred_edgeL in Iq. apply/andP; split. -- apply: contraNneq xp => <-. by rewrite mem_path A mem_cat -!(@mem_path del_edge) path_begin. -- apply: contraTneq Ip => ?. subst z. rewrite irredE A cat_uniq [has _ _](_ : _ = true) //. apply/hasP. by exists b => /=; rewrite -!(@mem_path del_edge) path_begin. + case: (boolP ((x : del_edge) -- z)) => [xzD|xzND]. * right. have Iq : irred (pcat (edgep xzD) p1). { by rewrite irred_edgeL (valP p1) mem_path -E -(@mem_path G) xp. } exists (Sub _ Iq). by rewrite !nodes_pcat E. * left. rewrite /edge_rel/= xz /= negb_or !negbK in xzND. case/andP : xzND => /eqP ? /eqP ?. subst x. subst z. have Iq : irred (@idp del_edge a) by apply: irred_idp. exists (Sub _ Iq). exists p1. split => //=. -- by rewrite nodes_pcat E [nodes p1]nodesE /= -cat1s catA !nodesE. -- by rewrite (@mem_path del_edge) -E -(@mem_path G). -- rewrite (@mem_path del_edge) nodesE /= inE. apply: contraNneq xp => <-. by rewrite mem_path E -(@mem_path del_edge) path_begin. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)