case mk
n m : ℕ
b : Fin n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑({ val := val✝, isLt := isLt✝ } - b) = (↑{ val := val✝, isLt := isLt✝ } + (n - ↑b)) % n
n m : ℕ
a b : Fin n
⊢ ↑(a - b) = (↑a + (n - ↑b)) % n
cases a
case mk.mk
n m val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑({ val := val✝¹, isLt := isLt✝¹ } - { val := val✝, isLt := isLt✝ }) =
    (↑{ val := val✝¹, isLt := isLt✝¹ } + (n - ↑{ val := val✝, isLt := isLt✝ })) % n
case mk
n m : ℕ
b : Fin n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑({ val := val✝, isLt := isLt✝ } - b) = (↑{ val := val✝, isLt := isLt✝ } + (n - ↑b)) % n
cases b
no goals
case mk.mk
n m val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑({ val := val✝¹, isLt := isLt✝¹ } - { val := val✝, isLt := isLt✝ }) =
    (↑{ val := val✝¹, isLt := isLt✝¹ } + (n - ↑{ val := val✝, isLt := isLt✝ })) % n
rfl