proposition: Lemma jump_add : forall i j l, jump (i + j) l = jump i (jump j l).
proof: Proof. intro i; induction i as [|i IHi] using Pos.peano_ind; intros. - now rewrite Pos.add_1_l, jump_succ. - now rewrite Pos.add_succ_l, !jump_succ, IHi. Qed.
imports: BinPos List