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