proposition: Lemma jump_succ : forall j l, jump (Pos.succ j) l = jump 1 (jump j l).
proof: Proof. intro j;induction j as [j IHj|j IHj|];simpl;intros. - rewrite !IHj; simpl; now rewrite !jump_tl. - now rewrite !jump_tl. - trivial. Qed.
imports: BinPos List