English
Let m and n be positive integers and a an element of ZMod m. Then the representative of a when regarded as an element of ZMod n (i.e., (a.cast).val) is strictly less than m.
Русский
Пусть m и n положительные целые, возьмём a ∈ ZMod m. Тогда представление a при рассмотрении как элемента ZMod n имеет величину, строго меньшую m.
LaTeX
$$$ (a.cast : \mathbb{Z}/n\mathbb{Z}).\mathrm{val} < m $$$
Lean4
theorem val_cast_zmod_lt {m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) : (a.cast : ZMod n).val < m :=
by
rcases m with (⟨⟩ | ⟨m⟩); · cases NeZero.ne 0 rfl
by_cases h : m < n
· rcases n with (⟨⟩ | ⟨n⟩); · simp at h
rw [← natCast_val, val_cast_of_lt]
· apply a.val_lt
apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h
· rw [not_lt] at h
apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))
