Small values that differ by a multiple of a large value

Stream: Is there code for X?

[Bolton Bailey]

Do we have a theorem like this somewhere?

lemma near_small (a b d : ℕ) (c : ℤ) (ha : a < d) (hb : b < d) (habcd : a = b + c * d) :
    c = 0 := by
  sorry

[Bolton Bailey]

Shouldn't this be the kind of lemma that omega proves?

[Junyan Xu]

omega could handle multiplication by a constant but not necessarily arbitrary ones. You may try to use docs#Nat.ModEq.eq_of_lt_of_lt.

[Bolton Bailey]

Thanks. I came up with

lemma mod_cast_eq_cast_mod (a b : ℕ) : ((a : ℤ) % (b : ℤ)) = ((a % b : ℕ): ℤ) := by
  exact rfl

lemma near_mods (a b d : ℕ) (c : ℤ) (ha : a < d) (hb : b < d) (habcd : a = b + c * d) :
    c = 0 := by
  have h := congr_arg (fun p => p % (d : ℤ)) habcd
  simp at h
  rw [mod_cast_eq_cast_mod] at h
  rw [mod_cast_eq_cast_mod] at h
  rw [Int.ofNat_inj] at h
  simp [ha,hb, Nat.mod_eq_of_lt]  at h -- Why isn't the lemma simp tagged?
  rw [h] at habcd
  simp at habcd
  cases habcd <;> linarith

[Junyan Xu]

lemma near_mods (a b d : ℕ) (c : ℤ) (ha : a < d) (hb : b < d) (habcd : a = b + c * d) :
    c = 0 := by
  have : a = b := Nat.ModEq.eq_of_lt_of_lt (m := d) (Nat.modEq_of_dvd <| by simp [habcd]) ha hb
  simp_all [(a.zero_le.trans_lt ha).ne']