proposition: Lemma rev_path x p : path e (last x p) (rev (belast x p)) = path (fun z => e^~ z) x p.
proof: Proof. elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC. by rewrite -(last_cons x) -rev_rcons -lastI rev_cons last_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)