proposition: Lemma path_last_nat n s x : path ord x s -> ord x (last x s).+(n+1).
proof: Proof. move: n s x. suff L: forall s x, path ord x s -> ord x (last x s).+(1). - elim=>[|n IH] // s x; move/IH=>E; apply: trans E _. by case: (last x s)=>m; rewrite /ord /= addSn (addnS m). elim=>[|y s IH x] /=; first by case=>x; rewrite /ord /= addn1. by case/andP=>H1; move/IH; apply: trans H1. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)