aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Intuition.v
blob: 5f1914d21f1cae81e2155349ae11759daccdf6aa (plain)
1
2
3
4
5
Require Import ZArith_base.
Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z.
intros; intuition.
Show.
Abort.