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.
|
