How to perform finite step induction?

Stream: Is there code for X?

[Junqi Liu]

I wanna to prove the following example, I think it need to do finite step induction. But I don't find corresponding theorem.

import Mathlib

structure qqq (n : ℕ) where
  board : (Fin n × Fin n) → (Finset.Icc 1 (n ^ 2))
  bij : Function.Bijective board

example {n : ℕ} (sq : qqq n) (x : RelSeries (α := Fin n × Fin n) (fun x y ↦ sq.board x < sq.board y))
  (m1 m2 : Fin (x.length + 1)) (hm : m1 < m2) (hx : ∀ (i : Fin x.length), sq.board (x.toFun i.castSucc) < sq.board (x.toFun i.succ)):
  sq.board (x m1) < sq.board (x m2) := by
  sorry

[Robin Arnez]

I'm not sure if you stated this entirely how it should be: The size of the RelSeries is completely independent from n here so what happens here is that it does two casts -- one to Nat and the other back to Fin. So let's say the RelSeries has length 3 and we have n = 7. Then the Fin (n + 1)s 0, 1, 2, 3, 4, 5, 6, 7 map to 0, 1, 2, 0, 1, 2, 0, 1. Regarding induction, there is probably some merit in doing induction on n, although I'm not entirely sure.

[Junqi Liu]

oh! my bad. I'll fix it