aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4717.v
blob: 1507fa4bf00e5539f4c41f8aa73137defb5fd2e2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
(* Omega being smarter on recognizing nat and Z *)

Require Import Omega.

Definition nat' := nat.

Theorem le_not_eq_lt : forall (n m:nat),
    n <= m ->
    n <> m :> nat' ->
    n < m.
Proof.
  intros.
  omega.
Qed.

Goal forall (x n : nat'), x = x + n - n.
Proof.
  intros.
  omega.
Qed.

Require Import ZArith ROmega.

Open Scope Z_scope.

Definition Z' := Z.

Theorem Zle_not_eq_lt : forall n m,
    n <= m ->
    n <> m :> Z' ->
    n < m.
Proof.
  intros.
  omega.
  Undo.
  romega.
Qed.