proposition: Lemma link_has_None (x y : link) (p q : Path x y) : irred p -> irred q -> None \in p -> None \in q.
proof: Proof. Proof using U_disc. move: x y p q => [x|] [y|] p q; try by rewrite ?(@path_end link) ?(@path_begin link). move => Ip Iq Np. apply: contraTT isT => Nq. case/(isplitP Ip) def_p : _ / Np => [p1 p2 Ip1 Ip2 I12]. subst. case: (splitL p2) => // [] [a|] [/= na] [p2'] [D _] //. case: (splitL (prev p1)) => // [] [b|] [/= nb] [p1'] [D' _] //. have ? : b = a; last subst. { suff [p Hp] : exists p : @Path link (Some b) (Some a), None \notin p. { exact: link_bypass Hp. } exists (pcat p1' (pcat q (prev p2'))). rewrite !(@mem_pcat link) mem_prev (negbTE Nq) /= negb_or. move: Ip1 Ip2. rewrite -irred_rev D' D !irred_edgeL. by do 2 case: (_ \notin _). } move: (I12 (Some a)). case/(_ _ _)/Wrap => //; rewrite ?mem_pcat ?path_end //. by rewrite -mem_prev D' mem_pcat path_begin. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)