bug_11270.v « micromega « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/micromega/bug_11270.v

blob: 80abc6d0e95c82342c6b6b0347d633742169fc79 (plain)

Require Import Psatz.
Theorem foo : forall a b, 1 <= S (a + a * S b).
Proof.
intros.
lia.
Qed.