case zero
n m : ℕ
a b : Fin zero
⊢ ↑(a - b) = zero + ↑a - ↑b ↔ a < b

case succ
n✝ m n : ℕ
a b : Fin (Nat.succ n)
⊢ ↑(a - b) = Nat.succ n + ↑a - ↑b ↔ a < b
n✝ m n : ℕ
a b : Fin n
⊢ ↑(a - b) = n + ↑a - ↑b ↔ a < b
cases' n with n
case succ
n✝ m n : ℕ
a b : Fin (Nat.succ n)
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
case succ
n✝ m n : ℕ
a b : Fin (Nat.succ n)
⊢ ↑(a - b) = Nat.succ n + ↑a - ↑b ↔ a < b
rw [lt_iff_val_lt_val, Fin.coe_sub, add_comm]
case succ.inl
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑b ≤ ↑a
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b

case succ.inr
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑a < ↑b
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
case succ
n✝ m n : ℕ
a b : Fin (Nat.succ n)
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
cases' le_or_lt (b : ℕ) a with h h
no goals
case zero
n m : ℕ
a b : Fin zero
⊢ ↑(a - b) = zero + ↑a - ↑b ↔ a < b
exact @finZeroElim (fun _ => _) a
case succ.inl
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑b ≤ ↑a
⊢ ¬(Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b
case succ.inl
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑b ≤ ↑a
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
refine iff_of_false ?_ (not_lt_of_le h)
no goals
case succ.inl
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑b ≤ ↑a
⊢ ¬(Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b
simpa [add_tsub_assoc_of_le h] using
  ((Nat.mod_lt _ (Nat.succ_pos _)).trans_le le_self_add).ne
case succ.inr
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑a < ↑b
⊢ a < b
case succ.inr
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑a < ↑b
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
simp [← tsub_tsub_assoc b.is_lt.le h.le, ← tsub_add_eq_add_tsub b.is_lt.le,
  Nat.mod_eq_of_lt (tsub_lt_self (Nat.succ_pos _) (tsub_pos_of_lt h)), val_fin_le.mp _]
no goals
case succ.inr
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑a < ↑b
⊢ a < b
exact h