proposition: Lemma nth_jump : forall p l, nth p (tl l) = hd default (jump p l).
proof: Proof. intro p;induction p as [p IHp|p IHp|];simpl;intros. - now rewrite <-jump_tl, IHp. - now rewrite <-jump_tl, IHp. - trivial. Qed.
imports: BinPos List