diff options
Diffstat (limited to 'test-suite/micromega/rexample.v')
| -rw-r--r-- | test-suite/micromega/rexample.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 52dc9ed2e0..354c608e23 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -24,6 +24,16 @@ Proof. lra. Qed. +Goal + forall (a c : R) + (Had : a <> a), + a > c. +Proof. + intros. + lra. +Qed. + + (* Other (simple) examples *) Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2). @@ -32,7 +42,6 @@ Proof. lra. Qed. - Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m. Proof. intros ; lra. |