English
For Fin n, a < a - b iff a < b (under appropriate n).
Русский
Для Fin n верно, что a < a - b эквивалентно a < b (при соответствующем n).
LaTeX
$$$\\forall {n},\\forall {a,b}\\in \\mathrm{Fin}(n),\\; a < a-b \\iff a < b$$$
Lean4
@[simp]
theorem lt_sub_iff {n : ℕ} {a b : Fin n} : a < a - b ↔ a < b :=
by
rcases n with - | n
· exact a.elim0
constructor
· contrapose!
intro h
obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_le (Fin.not_lt.mp h)
simpa only [Fin.not_lt, le_iff_val_le_val, sub_def, hl, ← Nat.add_assoc, Nat.add_mod_left, Nat.mod_eq_of_lt,
Nat.sub_add_cancel b.is_lt.le] using (le_trans (mod_le _ _) (le_add_left _ _))
· intro h
rw [lt_iff_val_lt_val, sub_def]
simp only
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt b.is_lt
have : n + 1 - b = k + 1 := by
simp_rw [hk, Nat.add_assoc, Nat.add_sub_cancel_left]
-- simp_rw because, otherwise, rw tries to rewrite inside `b : Fin (n + 1)`
rw [this, Nat.mod_eq_of_lt (hk.ge.trans_lt' ?_), Nat.lt_add_left_iff_pos] <;> omega
