blob: 2825701410af48b599504b46316080f0ebd6334a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
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.
|