Intuition.v « output « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/output/Intuition.v

blob: a6173561718699130d48a0de37fe5d8aaf2e2874 (plain)

Require ZArith_base.
Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`.
Intros; Intuition.
Show.