Why do we have both `nat.dvd_sub` and `nat.dvd_sub'`?

Stream: new members

[Martin C. Martin]

They're the same, except the unprimed one has an extra hypothesis, n ≤ m. If the conclusion holds without the hypothesis, then why do we have another version that needs that hypothesis? Something to do with truncating subtraction?

[Martin C. Martin]

From the source:

-- TODO: update `nat.dvd_sub` in core
lemma dvd_sub' {k m n : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=

So I guess the TODO is agreeing with me, that we should drop the unneeded hypothesis? But that's a lot of work, because you need to update everywhere that it's used?

[Ruben Van de Velde]

More importantly, changing lemmas in core lean 3 is more of a pain than changing something in mathlib

[Ruben Van de Velde]

I suspect a refactor like this would not be particularly welcome during the port to lean 4

[Mario Carneiro]

Since both versions are headed for mathlib4, it will be much easier to do the refactor on the other side. The way to do so while preserving backward compatibility is to define both dvd_sub and dvd_sub' with their stated signatures unchanged, but prove dvd_sub trivially using dvd_sub' and mark it as @[deprecated dvd_sub'] so that downstream uses can be refactored.

[Mario Carneiro]

It is also possible to move the ' to the old definition and use #align statements to swap things around