theorem Fin.coe_succ_le_iff_le {n : ℕ} {j k : Fin n} : ↑↑j ≤ ↑↑k ↔ j ≤ k

theorem Fin.coe_lt_succ {n : ℕ} (k : Fin n) : ↑↑k < k.succ