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