Val Min Abs nat Abs le

theorem valMinAbs_natAbs_le {a : ZMod q} (m : ℤ) (h : (m : ZMod q) = a) :    a.valMinAbs.natAbs ≤ m.natAbs := by  have hmem := ZMod.valMinAbs_mem_Ioc a  rw [Set.mem_Ioc] at hmem  have hcast : (m : ZMod q) = ((a.valMinAbs : ℤ) : ZMod q) := by rw [h, ZMod.coe_valMinAbs]  rw [ZMod.intCast_eq_intCast_iff_dvd_sub] at hcast  obtain ⟨t, ht⟩ := hcast  have hq : (1 : ℤ) ≤ (q : ℤ) := by exact_mod_cast Nat.one_le_iff_ne_zero.mpr (NeZero.ne q)  rcases eq_or_ne t 0 with ht0 | ht0  · subst ht0; simp only [mul_zero] at ht; omega  · have habs : q ≤ ((q : ℤ) * t).natAbs := by      have ht1 : 1 ≤ t.natAbs := Int.natAbs_pos.mpr ht0      rw [Int.natAbs_mul]; simp only [Int.natAbs_natCast]; nlinarith [ht1]    revert ht habs    generalize (q : ℤ) * t = k    intro ht habs    omega