test-suite/bugs/opened/bug_1615.v


1
2
3
4
5
6
7
8
9
10
11

Require Import Omega.

Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
Proof.
  intros. omega.
Qed.

Lemma foo' : forall n m : nat, n <=  n + n * m.
Proof.
  intros. Fail omega.
Abort.