blob: 3690adf90a8fde9dbe259c5b454ff1677eb58567 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Require Import Omega.
Lemma test_nat:
forall n, (5 + pred n <= 5 + n).
Proof.
intros.
zify.
omega.
Qed.
Lemma test_N:
forall n, (5 + N.pred n <= 5 + n)%N.
Proof.
intros.
zify.
omega.
Qed.
|