feat(Nat): m / n = 0 ↔ n = 0 ∨ m < n

[YaelDillies]

From LeanCamCombi

---

[github-actions]

PR summary 04f3842e4c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Command-Master]

Could you add "Moves: ..." to the PR description, as you can't deprecate the old names? Another option which I recall being taken once is to keep the old lemma's name, deprecate it, and use div_eq_zero_iff' for now

[YaelDillies]

Could you add "Moves: ..." to the PR description, as you can't deprecate the old names?

Confusingly (cc @eric-wieser), "Moves" means "renames", not "statement change" nor "relocation". So this PR contains no "Move".

[eric-wieser]

Perhaps I read this PR wrong, but if I have

theorem a : A
theorem b : B

and change it to

theorem b : A
theorem c : B

then this should be recorded as a move from a to b and a move from b to c, not as a "statement change" of b.

[YaelDillies]

Then do you want me to add
Moves:

• Nat.div_eq_zero_iff -> ``
• Nat.div_ne_zero_iff -> ``
• Nat.div_pos_iff -> ``

to the PR description? A less silly way to look at things is that I strengthened three lemmas.