From 28a38529e47d2593a7af41a7223208e2dd049179 Mon Sep 17 00:00:00 2001 From: fbesson Date: Mon, 11 May 2009 20:09:34 +0000 Subject: micromega: proof compression bugfix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12123 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/micromega/zomicron.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'test-suite/micromega') 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 -- cgit v1.2.3