test-suite/bugs/opened/6602.v


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.