Hi all!

I'm looking for some kind of catalog of elementary proofs made in Coq I remember to have spotted once. For instance things like x*y = 0 => x=0 or y=0 (on integers, rationals, real numbers).

I guess for things that are "elementary" in the sense of your example, no such catalog exists, nor would it be useful given that there are probably thousands of them, if not tens of thousands. If you are looking for something specific, the `Search`

command is your friend. However, it only searches in libraries that are currently loaded (via `Require`

, not necessarily imported). For instance, if you have loaded `ssrnat`

from `mathcomp`

, then

`Search (_ * _ == 0).`

returns:

```
muln_eq0: forall m n : nat, (m * n == 0) = (m == 0) || (n == 0)
```

as one of two results.

Last updated: Jun 25 2024 at 19:01 UTC