Division with remainder

Stream: new members

[Iocta]

Is there a theorem like this?

import Mathlib

example (n d : Nat) (hd : 0 < d) : ∃ (q r : Nat), r < d ∧ n = d * q + r := by
  induction n with
  | zero => {
    use 0
    use 0
    omega
  }
  | succ q hq => {
    obtain ⟨q', ⟨r', ⟨hr'd, hq⟩⟩⟩ := hq
    rw [hq]
/-
case succ.intro.intro.intro
d : ℕ
hd : 0 < d
q q' r' : ℕ
hr'd : r' < d
hq : q = d * q' + r'
⊢ ∃ q, ∃ r < d, d * q' + r' + 1 = d * q + r
-/

  }

[Damiano Testa]

The pieces are all available:

example (n d : Nat) (hd : 0 < d) : ∃ (q r : Nat), r < d ∧ n = d * q + r := by
  use n / d
  use n % d
  constructor
  · exact Nat.mod_lt n hd
  · exact (Nat.div_add_mod n d).symm

[Isak Colboubrani]

What would be the idiomatic formulation of this more generally in the context of Euclidean domains (instead of Nat)?

[Ruben Van de Velde]

See docs#EuclideanDomain

[Chris Wong]

See also docs#Nat.divModEquiv