I found the definition of axiomatic real numbers here.

Is `RInv R0`

a point in `R`

?

What will happen if you define `0 * / 0 = 1`

?

https://coq.inria.fr/distrib/8.4pl5/stdlib/Coq.Reals.Raxioms.html# ensures that `Rinv r`

is the inverse of `r`

:

```
Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
```

beware that's the stdlib of Coq 8.4, you probably want https://coq.inria.fr/stdlib/ instead

Locria Cyber said:

What will happen if you define

`0 * / 0 = 1`

?

If you set this equality as axiom, then you can trivially deduce `False`

, since you also have the equality `0 * foo = 0`

by virtue of zero being absorbing for the multiplication.

Last updated: Jun 14 2024 at 18:01 UTC