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
Search (_ * _ == 0). returns:
muln_eq0: forall m n : nat, (m * n == 0) = (m == 0) || (n == 0)
as one of two results.
Last updated: Jan 31 2023 at 14:03 UTC