aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1912.v
blob: 987a54177809d076263a93b6baaf89401dc4796b (plain)
1
2
3
4
5
6
Require Import ZArith.

Goal forall x, Z.succ (Z.pred x) = x.
intros x.
omega.
Qed.