The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

This is from the definition of "minus" in Coq with infix notation "x - y".
"Print minus" will give you the fixpoint definition.
 
If a <= b then  a-b = 0. You can prove this. 

You just have to be aware that this is not the usual subtraction 
operation which would be a partial operation on natural numbers 
(positive integers), ie a-b should be undefined when a < b.

a - b has the "usual" meaning if (and only if) a >= b.

This is enough to get (a + b) - b = a for instance
But (a - b) + b is not equal to a, unless a >= b.

Best,

Dominique

----- Mail original -----
> De: "Frank Schwidom" <schwidom AT gmx.net>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Dimanche 23 Juillet 2023 16:53:35
> Objet: [Coq-Club] Beginner question: 0 - 1 = 0?

> Hi,
> 
> what puzzles me is that I can obviously get a wromg result from the view of 
> the
> natural understanding:
> 
> Coq < Compute 0 - 1.
>     = 0
>     : nat
> 
> How can it be clear that this makes no problems in proofs?
> 
> Regards,
> Frank