diff options
Diffstat (limited to 'test-suite/micromega/zomicron.v')
| -rw-r--r-- | test-suite/micromega/zomicron.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 3087db1ad..60c16a998 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -26,3 +26,11 @@ Proof. lia. Qed. +Lemma compact_proof : forall z, + (z < 0) -> + (z >= 0) -> + (0 >= z \/ 0 < z) -> False. +Proof. + intros. + lia. +Qed.
\ No newline at end of file |