proposition: Lemma path_connect x p : path e x p -> subpred [in x :: p] (connect x).
proof: Proof. move=> e_p y p_y; case/splitPl: p / p_y e_p => p q <-. by rewrite cat_path => /andP[e_p _]; apply/connectP; exists p. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)