blob: bd9bac37ef1377134e6e66fa67da8ea2aaafeb47 (
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
|
(* 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.
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.
Qed.
|
