-lemma at_monotonic: ∀cs,i2,j2. @⦃i2, cs⦄ ≡ j2 → ∀i1. i1 < i2 →
- ∃∃j1. @⦃i1, cs⦄ ≡ j1 & j1 < j2.
-#cs #i2 #j2 #H elim H -cs -i2 -j2
-[ #cs #i1 #H elim (lt_zero_false … H)
-| #cs #i #j #Hij #IH * /2 width=3 by ex2_intro, at_zero/
- #i1 #H lapply (lt_S_S_to_lt … H) -H
- #H elim (IH … H) -i
- #j1 #Hij1 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
-| #cs #i #j #_ #IH #i1 #H elim (IH … H) -i
+(* Note: lemma 250 *)
+lemma at_le: ∀cs,i1. i1 ≤ ∥cs∥ →
+ ∃∃i2. @⦃i1, cs⦄ ≡ i2 & i2 ≤ |cs|.
+#cs elim cs -cs
+[ #i1 #H <(le_n_O_to_eq … H) -i1 /2 width=3 by at_empty, ex2_intro/
+| * #cs #IH
+ [ * /2 width=3 by at_zero, ex2_intro/
+ #i1 #H lapply (le_S_S_to_le … H) -H
+ #H elim (IH … H) -IH -H /3 width=3 by at_succ, le_S_S, ex2_intro/
+ | #i1 #H elim (IH … H) -IH -H /3 width=3 by at_false, le_S_S, ex2_intro/
+ ]
+]
+qed-.
+
+lemma at_top: ∀cs. @⦃∥cs∥, cs⦄ ≡ |cs|.
+#cs elim cs -cs // * /2 width=1 by at_succ, at_false/
+qed.
+
+lemma at_monotonic: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀j1. j1 < i1 →
+ ∃∃j2. @⦃j1, cs⦄ ≡ j2 & j2 < i2.
+#cs #i1 #i2 #H elim H -cs -i1 -i2
+[ #j1 #H elim (lt_zero_false … H)
+| #cs #j1 #H elim (lt_zero_false … H)
+| #cs #i1 #i2 #Hij #IH * /2 width=3 by ex2_intro, at_zero/
+ #j1 #H lapply (lt_S_S_to_lt … H) -H
+ #H elim (IH … H) -i1
+ #j2 #Hj12 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
+| #cs #i1 #i2 #_ #IH #j1 #H elim (IH … H) -i1