coe_sub_one — Mathlib

English

For all a,b in Fin n, rev(a + b) = rev a - b.

Русский

Для любых a,b в Fin n выполняется rev(a + b) = rev a - b.

LaTeX

$$$\\forall a,b\\in \\mathrm{Fin}(n),\\; \\text{rev}(a+b)=\\text{rev}(a)-b$$$

Lean4

theorem coe_sub_one (a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else a - 1 :=
  by
  cases n
  · simp
  split_ifs with h
  · simp [h]
  rw [sub_eq_add_neg, val_add_eq_ite, coe_neg_one, if_pos, Nat.add_comm, Nat.add_sub_add_left]
  conv_rhs => rw [Nat.add_comm]
  rw [Nat.add_le_add_iff_left, Nat.one_le_iff_ne_zero]
  rwa [Fin.ext_iff] at h

Похожие утверждения