For some reason,
coq-hammer can't solve the following simple goal with
exists (I have all supported ATPs installed).
From Hammer Require Import Hammer. From Hammer Require Import Tactics. Require Import ZArith. Open Scope Z_scope. Goal exists (n : Z), n + 50 > 100. hammer.
What is the reason for this and how can I solve such goals automatically? I know that Z3 can easily find
n = 51 for instance.
Last updated: Jan 31 2023 at 12:01 UTC