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

case succ
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a
n✝ m n : ℕ
a b : Fin n
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a
cases n
case succ
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
case succ
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a
rw [le_iff_val_le_val, Fin.coe_sub, ← add_tsub_assoc_of_le b.is_lt.le a]
case succ.inl
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑b ≤ ↑a
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a

case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
case succ
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
cases' le_or_lt (b : ℕ) a with h h
no goals
case zero
n m : ℕ
a b : Fin zero
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a
exact @finZeroElim (fun _ => _) a
no goals
case succ.inl
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑b ≤ ↑a
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
simp [← tsub_add_eq_add_tsub h, val_fin_le.mp h,
  Nat.mod_eq_of_lt ((Nat.sub_le _ _).trans_lt a.is_lt)]
case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ ¬↑a + Nat.succ n✝ ≤ ↑b ↔ ¬↑b ≤ ↑a

case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ ↑a + Nat.succ n✝ - ↑b < Nat.succ n✝
case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
rw [Nat.mod_eq_of_lt, tsub_eq_zero_of_le h.le, tsub_eq_zero_iff_le, ← not_iff_not]
no goals
case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ ¬↑a + Nat.succ n✝ ≤ ↑b ↔ ¬↑b ≤ ↑a
simpa [b.is_lt.trans_le le_add_self] using h
no goals
case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ ↑a + Nat.succ n✝ - ↑b < Nat.succ n✝
rwa [tsub_lt_iff_left (b.is_lt.le.trans le_add_self), add_lt_add_iff_right]