English
For k ≤ n, addRothNumber(Iio(k)) ≤ rothNumberNat(k).
Русский
Для k ≤ n выполняется addRothNumber(Iio(k)) ≤ rothNumberNat(k).
LaTeX
$$$\\operatorname{addRothNumber}(\\mathrm{Iio}(k)) \\le \\operatorname{rothNumberNat}(k).$$$
Lean4
theorem addRothNumber_le_rothNumberNat (k n : ℕ) (hkn : k ≤ n) :
addRothNumber (Iio k : Finset (Fin n.succ)) ≤ rothNumberNat k :=
by
suffices h : Set.BijOn (Nat.cast : ℕ → Fin n.succ) (range k) (Iio k : Finset (Fin n.succ)) by
exact (AddMonoidHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h
refine ⟨?_, (CharP.natCast_injOn_Iio _ n.succ).mono (by simp; cutsat), ?_⟩
· simpa using fun x ↦ natCast_strictMono hkn
simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_iff_val_lt_val, val_cast_of_lt,
Nat.lt_succ_iff.2 hkn, coe_range]
exact fun x hx ↦ ⟨x, hx, by simp⟩
