proposition: Lemma nexts_plus : forall n p q , nexts (n+p) q = match (nexts n q) with Some q' => nexts p q' | None => None end.
proof: Proof. induction n;simpl. auto. intros; case (next q). intro s; case s;auto. auto. Qed.
imports: Arith Omega Relations