proposition: Lemma nth_spec p l : nth p l = match p with | xH => hd l | xO p => nth p (jump p l) | xI p => nth p (jump p (tail l)) end.
proof: Proof. unfold hd, nth, tail, jump. destruct p; f_equal; now rewrite Pos.add_diag. Qed.
imports: BinInt List