diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 23:23:36 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 23:23:36 +0200 |
| commit | e65c629bac48e61b3a14f05bfafc6b85486359c0 (patch) | |
| tree | 0e76cddb78a62eb9bd6bbf9ec8382fdfdf6f2cbb /test-suite/micromega/rexample.v | |
| parent | ef3f9fac7cff820bd927d122caef2c37a68a55c8 (diff) | |
Fix Bug #5073 : regression of micromega plugin
esprit d'escalier : is now also fixed for R
Diffstat (limited to 'test-suite/micromega/rexample.v')
| -rw-r--r-- | test-suite/micromega/rexample.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 12f72a580..bd5227010 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -81,3 +81,8 @@ Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). intros; split_Rabs; lra. Qed. +(* Bug 5073 *) +Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. +Proof. + lra. +Qed. |