How to interpret conflicting formal proofs about "a mod 0 = ? " 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

 A: If $a$ mod 0 is to be defined at all (and I'm not entirely convinced that it should be), then it ought to differ from $a$ by a multiple of 0, which means to me that it ought to be $a$.  But it's asserted in the question that the computer systems have a strange notion of division by 0, so they might think that everything is a multiple of 0.  In this alternative "reality", everything is congruent to everything else modulo 0; so if you define $a$ mod $b$ as the smallest non-negative integer congruent to $a$ modulo $b$, then $a$ mod 0 would be 0.  Personally, I refuse to buy into this alternative reality; congruence modulo 0 should mean equality.  (Fortunately, I rarely use computer algebra systems, and I have never yet asked one about divisibility by 0.)
A: In the logic of Isabelle/HOL, nothing can be undefined. For a partial function such as division, the best we can do is complete the definitions in the most plausible manner, retaining as many well-known facts as possible (preferably unconditionally). Defining division such that x/0=0 (for integers, reals, etc.) works quite well. The Isabelle definitions also ensure that
"a div b * b + a mod b = a"
holds unconditionally.
Coq has dependent types, and in principle the type of div and mod could ensure that the second argument was nonzero. I don't know why this is not done.
