+
+(* Basic properties *********************************************************)
+
+lemma nexts_le: ∀h,k,l. k ≤ (next h)^l k.
+#h #k #l elim l -l // normalize #l #IHl
+lapply (next_lt h ((next h)^l k)) #H
+lapply (le_to_lt_to_lt … IHl H) -IHl -H /2 width=2/
+qed.
+
+axiom nexts_dec: ∀h,k1,k2. Decidable (∃l. (next h)^l k1 = k2).
+
+axiom nexts_inj: ∀h,k,l1,l2. (next h)^l1 k = (next h)^l2 k → l1 = l2.
+