I'm trying to find the discussion on division by zero mentioned in #11447.

My main concern is the design decision leading to the incoherence

```
Compute (1 mod 0)%nat. (* = 0%nat : nat *)
Compute (1 mod 0)%Z. (* = 0%Z : Z *)
Compute (1 mod 0)%N. (* = 1%N : N *)
```

Annoyed by the glue code / superfluous assumptions I created PR #14086 to address the described issue. Now computation is uniform and we have `n = (n / m) * m + (n mod m)`

in `nat`

, `N`

, (nonnegative) `Z`

.

@Enrico Tassi do you know the rationale behind `math-comp`

's `Lemma modn0 m : m %% 0 = m.`

(which breaks away from current Coq's `m mod 0 = 0`

design decision)?

I don't but this question may get a better in asnwer in math-comp users

Would you mind asking on that stream?

For those who are interested: the PR #14086 (for uniform modulo treatment) is ready, requiring maintainers review/approval. Once accepted, we can have a uniform `div`

, `mod`

lemmas for `lia`

/`nia`

(see follow up PR #14037).

Last updated: Jun 14 2024 at 19:02 UTC