The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$.

According to Coq $$ a \mod 0 = 0$$ and Isabelle proves $$ a \mod = a$$

`mod`

is the function, not a congruence.

Which way is it?

All the computer algebra systems I tried give an error in this case.

Can one derive a counter intuitive statement from the above results?

Both agree that integer division by $0$ is $0$ forall $\mathbb{Z}$.

Coq proof:

```
Require Import ZArith.
Require Import Coq.ZArith.Znumtheory.
Open Scope Z_scope.
Lemma mod0: forall n:Z, n mod 0 = 0.
apply Zmod_0_r.
Qed.
```

Isabelle proof:

```
theory mod0
imports Main
begin
lemma mod0: " \<forall> n \<in> \<int>. n mod (0::int) = n"
by auto
```

`int`

or $2+2$? – joro Nov 29 '11 at 16:24nothave a generally accepted meaning. – Thierry Zell Nov 29 '11 at 17:39`mod`

in a more traditional way:`div_mod : forall n1 n2, n2 > 0 -> {p1 | p1 = (n3, n4) -> n1 = n3 * n2 + n4 /\ n4 < n2}`

. The difference between`exists x1, p1 x1`

and`{x1 | p1 x1}`

is that the first is a`Prop`

and the second is a`Set`

or`Type`

.`Definition mod : forall n1 n2, n2 > 0 -> nat * nat := fun n1 n2 h1 => snd (proj1_sig (div_mod n1 n2 h1))`

. – Rui Baptista Dec 7 '13 at 15:41