RS.IPart.exists_index_between

lemma exists_index_between {n m : ℕ} (k : Fin (n + 1) → Fin (m + 1))  (hk : Monotone k) (hk0 : k 0 = 0) (hkn : k (Fin.last n) = Fin.last m)  (j : Fin m) :  ∃ i : Fin n, k i.castSucc ≤ j.castSucc ∧ j.castSucc < k i.succ := by    by_contra h_contra;    -- Since $k$ is monotone and $k 0 = 0$, we have $k i \le j$ for all $i$.    have h_le : ∀ i : Fin (n + 1), k i ≤ Fin.castSucc j := by      intro i; induction i using Fin.inductionOn <;> aesop;    exact absurd ( h_le ( Fin.last n ) ) ( by simpa [ hkn ] using Fin.castSucc_lt_last j )