diff options
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. |