English
For u,v in Fin(n), the integer value of u − v is u.val − v.val plus 0 if v ≤ u, else plus n; i.e., the wrap around.
Русский
Для u,v ∈ Fin(n) целочисленное значение u−v равно u.val − v.val плюс 0, если v ≤ u, иначе плюс n; то есть обход вокруг кольца мод n.
LaTeX
$$$$((u-v)\,:\\mathbb{Z}) = (u_{\mathrm{val}}-v_{\mathrm{val}}) + \begin{cases}0,& v\le u,\\ \\ n,& \text{otherwise} \end{cases}.$$$$
Lean4
theorem coe_int_sub_eq_ite {n : Nat} (u v : Fin n) :
((u - v : Fin n) : Int) = if v ≤ u then (u - v : Int) else (u - v : Int) + n :=
by
rw [Fin.sub_def]
split
· rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> omega
· rw [natCast_emod, Int.emod_eq_of_lt] <;> omega
