proposition: Lemma pdfs_connect s x : x \in s -> let (s1, l1) := pdfs (s, [::]) x in [/\ uniq l1, s1 = s :\: [set x in l1], l1 \subset s & forall y, y \in l1 = x -[[pred u in s]]-> y].
proof: Proof. move=> xIs. set p := (_, _). have UN : [/\ uniq p.2 & {subset p.2 <= ~: p.1}] by []. case: pdfs (pdfs_correct (_, _) x UN) => s1 l1. rewrite xIs => /=[[[_ Ul1] [l2 [xIl2 s1E l1E WH Cy]]]]. split => // [||y]. - by apply/setP=> i; rewrite s1E l1E !inE cats0. - apply/subsetP=> z. rewrite l1E cats0. by have [/subsetP/(_ z)/=] := WH. apply/idP/idP => [|H]. by rewrite l1E cats0; exact: Cy. rewrite l1E cats0. by have [_ /(_ x y xIl2 H)] := WH. Qed.
imports: mathcomp(all_ssreflect) extra