proposition: Fact theta_vertices (G : diGraph) (x y : G) s (p : 'I_s -> IPath x y) : x != y -> ~~ x -- y -> exists (f : 'I_s -> G), forall i, f i \in interior (p i).
proof: Proof. move => xDy xNy. suff S i : { s | s \in interior (p i) }. { exists (fun i => val (S i)) => i. exact: (svalP (S i)). } case: (set_0Vmem (interior (p i))) => [I0|//]. exfalso. case: (interior0E xDy (valP (p i)) I0) => xy. by rewrite xy in xNy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)