Modulo characterization for Nat

Stream: Is there code for X?

[Siddharth Bhat]

example (m k : Nat) : m % k = m - k * (m / k) := by
  rw [Nat.sub_eq_of_eq_add]
  apply (Nat.mod_add_div _ _).symm

Does this exist in the library someplace? I tried loogling and looking, but failed to come up with anything. For Int, it's called Int.emod_def, and for ordinal, as Ordinal.mod_def. What should I name the Nat lemma?

[Siddharth Bhat]

I am tempted to call it Nat.mod_def.

[Ralf Stephan]

Somewhere in Data/Nat/ModEq?

[Ralf Stephan]

Term mode:

example (m k : Nat) : m % k = m - k * (m / k) :=
  Eq.symm (Nat.sub_eq_of_eq_add (Eq.symm (Nat.mod_add_div m k)))

[Ralf Stephan]

Better:

example (m k : Nat) : m % k = m - k * (m / k) :=
  Eq.symm <| Nat.sub_eq_of_eq_add <| Eq.symm <| Nat.mod_add_div m k

[Michael Stoll]

Or, using dot notation,

example (m k : Nat) : m % k = m - k * (m / k) :=
  (Nat.sub_eq_of_eq_add (Nat.mod_add_div m k).symm).symm