proposition: Lemma irred_in_sinterval (G : sgraph) (i o : G) (p : Path i o) : irred p -> {subset interior p <= sinterval i o}.
proof: Proof. move => Ip u. rewrite 5!inE negb_or -andbA => /and3P [U1 U2 U3]. case/(isplitP Ip) : U3 => {p Ip} p1 p2 Ip1 Ip2 I. apply/sintervalP2. split. - exists (prev p1); rewrite ?irred_rev // inE. apply: contraNN U2 => in_p. by rewrite [o]I. - exists p2 => //. apply: contraNN U1 => in_p. by rewrite [i]I. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)