test-suite/micromega/bug_12790.v


1
2
3
4
5
6
7
8

Require Import Lia.

Goal forall (a b c d x: nat),
S c = a - b -> x <= x + (S c) * d.
Proof.
intros a b c d x H.
lia.
Qed.