(* 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
(* 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