English
CastSucc commutes with predAbove: a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc.
Русский
CastSucc commuting предAbove: a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc.
LaTeX
$$$\forall a \in \mathrm{Fin}(n),\ \forall b \in \mathrm{Fin}(n+1),\ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc$$$
Lean4
/-- `castSucc` commutes with `predAbove`. -/
@[simp]
theorem castSucc_predAbove_castSucc {n : ℕ} (a : Fin n) (b : Fin (n + 1)) :
a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc :=
by
obtain h | h := a.castSucc.lt_or_ge b
· rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h, castSucc_pred_eq_pred_castSucc]
· rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]
