I tried to prove this with Coqhammer:

```
Theorem abc2 : exists k : nat * nat, fst k = 0 /\ snd k = 3
```

and it failed. I am wondering what the problem is here, is it with the use of product types?

This topic was moved to #Coq users > Coqhammer by Karl Palmskog.

Last updated: Nov 29 2023 at 21:01 UTC