# Zulip Chat Archive

## Stream: general

### Topic: hole? golf!

#### Johan Commelin (Apr 21 2020 at 12:10):

Is this a hole in the library? What is the shortest proof?

lemma dvd_sub_mod (k : ℕ) : n ∣ (k - (k % n)) :=

#### Kenny Lau (Apr 21 2020 at 12:14):

lemma dvd_sub_mod (n k : ℕ) : n ∣ (k - (k % n)) := ⟨k / n, nat.sub_eq_of_eq_add (nat.mod_add_div k n).symm⟩

#### Mario Carneiro (Apr 21 2020 at 12:16):

lemma dvd_sub_mod (n k : ℕ) : n ∣ k - k % n := ⟨k / n, (nat.sub_eq_iff_eq_add (nat.mod_le _ _)).2 $ (nat.mod_add_div _ _).symm.trans (add_comm _ _)⟩

#### Kenny Lau (Apr 21 2020 at 12:16):

yay my proof is shorter

#### Mario Carneiro (Apr 21 2020 at 12:18):

Damn you autocomplete

Screenshot-from-2020-04-21-05-17-09.png

#### Kenny Lau (Apr 21 2020 at 12:19):

looks like you have no imports?

#### Mario Carneiro (Apr 21 2020 at 12:19):

Oh, yes `import data.nat.basic`

solves the problem

#### Reid Barton (Apr 21 2020 at 12:21):

The nat subtraction makes this annoying.

lemma dvd_sub_mod (n k : ℤ) : n ∣ (k - (k % n)) := int.modeq.modeq_iff_dvd.mp (int.modeq.mod_modeq _ _)

#### Bhavik Mehta (Apr 21 2020 at 12:21):

Mario Carneiro said:

Damn you autocomplete

Screenshot-from-2020-04-21-05-17-09.png

(entirely unrelated - which theme is this? I quite like it)

#### Mario Carneiro (Apr 21 2020 at 12:22):

night owl

#### Johan Commelin (Apr 21 2020 at 12:22):

name checks out

#### Kenny Lau (Apr 21 2020 at 12:22):

cheater

#### Reid Barton (Apr 21 2020 at 12:24):

maybe another hole is, in `data.nat.modeq`

:

theorem modeq_iff_dvd_of_le (a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a

#### Mario Carneiro (Apr 21 2020 at 12:24):

I like the statement golfing

#### Reid Barton (Apr 21 2020 at 12:25):

removed an extraneous space to make it shorter

#### Mario Carneiro (Apr 21 2020 at 12:26):

I would skip the `of_le`

in the name

#### Mario Carneiro (Apr 21 2020 at 12:26):

unless you want another version when it's not `of_le`

#### Kenny Lau (Apr 21 2020 at 12:27):

The nonunits make this annoying.

import ring_theory.euclidean_domain data.real.basic lemma dvd_sub_mod (n k : ℝ) : n ∣ (k - (k % n)) := if H : n = 0 then by rw [H, euclidean_domain.mod_zero, sub_self] else ⟨(k - k % n) / n, by rw mul_div_cancel' _ H⟩

#### Reid Barton (Apr 21 2020 at 12:27):

There's an existing `theorem modeq_iff_dvd : a ≡ b [MOD n] ↔ (n:ℤ) ∣ b - a`

but maybe that should be the one with the altered name

#### Mario Carneiro (Apr 21 2020 at 12:28):

Yeah but that's in a different namespace, right?

#### Mario Carneiro (Apr 21 2020 at 12:29):

Oh I see this is for nats

#### Reid Barton (Apr 21 2020 at 12:29):

No this is for `nat`

s (`MOD`

is for `nat`

)--there's *also* `theorem modeq_iff_dvd : a ≡ b [ZMOD n] ↔ (n:ℤ) ∣ b - a :=`

in `int.zmod`

Last updated: May 16 2021 at 21:11 UTC