Division theorem

Stream: Is there code for X?

[Marcus Rossel]

Does there exist something like the following, or something that easily solves this?

example (h : d < b) (n : Nat) : (b * n + d) / b = n := by
  sorry

The idea is that given a "base-b number" b * n + d, dividing by the base just leaves n as d is irrelevant under natural number division. So for example 10 * 123 + 4 / 10 = 1234 / 10 = 123.

[Edward van de Meent]

example {b d : Nat} (n : Nat) (h₂ : d < b) : (b * n + d) / b = n := by
  rw [Nat.mul_comm]
  refine Nat.div_eq_of_lt_le ?_ ?_
  · exact Nat.le_add_right (n * b) d
  · rw [Nat.add_mul,Nat.one_mul]
    exact Nat.add_lt_add_left h₂ (n * b)

[Aaron Liu]

example {b d : Nat} (n : Nat) (h : d < b) : (b * n + d) / b = n := by
  rw [Nat.add_comm, Nat.mul_comm, Nat.add_mul_div_right d n (Nat.zero_lt_of_lt h),
    Nat.div_eq_of_lt h, Nat.zero_add]

[Markus Himmel]

Looking at the goal purely syntactically, you would hope for Nat.mul_add_div to exist, and this is in fact the case:

example {b d : Nat} (n : Nat) (h : d < b) : (b * n + d) / b = n := by
  rw [Nat.mul_add_div (by omega), Nat.div_eq_zero_iff.2 (by omega), Nat.add_zero]

[Marcus Rossel]

Ahhh, I was looking for div_mul_add :see_no_evil: