English
insertPerm a is a permutation of Fin2 n with the properties: insertPerm a i = i+1 if i < a; insertPerm a a = 0; insertPerm a i = i if i > a.
Русский
insertPerm a — перестановка Fin2 n с свойствами: если i < a, то insertPerm a i = i+1; a ↦ 0; если i > a, то insertPerm a i = i.
LaTeX
Lean4
/-- `insertPerm a` is a permutation of `Fin2 n` with the following properties:
* `insertPerm a i = i+1` if `i < a`
* `insertPerm a a = 0`
* `insertPerm a i = i` if `i > a` -/
def insertPerm : ∀ {n}, Fin2 n → Fin2 n → Fin2 n
| _, @fz _, @fz _ => fz
| _, @fz _, @fs _ j => fs j
| _, @fs (succ _) _, @fz _ => fs fz
| _, @fs (succ _) i, @fs _ j =>
match insertPerm i j with
| fz => fz
| fs k => fs (fs k)
