proposition: Lemma cat_path x p1 p2 : path x (p1 ++ p2) = path x p1 && path (last x p1) p2.
proof: Proof. by elim: p1 x => [|y p1 Hrec] x //=; rewrite Hrec -!andbA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)