proposition: Lemma pathP x p x0 : reflect (forall i, i < size p -> e (nth x0 (x :: p) i) (nth x0 p i)) (path x p).
proof: Proof. elim: p x => [|y p IHp] x /=; first by left. apply: (iffP andP) => [[e_xy /IHp e_p [] //] | e_p]. by split; [apply: (e_p 0) | apply/(IHp y) => i; apply: e_p i.+1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)