proposition: Lemma connectnP n x y : reflect (exists p : seq T, [/\ path r x p, last x p = y & size p = n]) (y \in connectn n x).
proof: Proof. elim: n x y => [x y|n IH x y /=]. rewrite inE; apply: (iffP idP) => [/eqP->|[[|a l] [] //= _ ->//]]. by exists [::]. apply: (iffP idP) => [/bigcupP[i]|[[|i p]//= [H1 H2 H3]]]. - rewrite [i \in _]rgraphK => iRk /IH [p [H1 H2 H3]]. by exists (i :: p); split; rewrite /= ?(iRk, H3). - by []. case/andP: H1 => H11 H12. have F : i \in rgraph r x by rewrite [_ \in _]rgraphK. apply: (subsetP (bigcup_sup _ F)). by apply/IH; exists p; split => //; case: H3. Qed.
imports: mathcomp(all_ssreflect)