[isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?

```Dear Isabelle experts,

```
somewhere in a proof that involves real numbers from the theory "Real" I would like to infer "(x::real) >= 0" from "x > 0".
```
For now I solved the problem by introducing the following axiomatic "lemma":

lemma greater_zero_implies_greater_equal_zero [simp] :
fixes x::real
assumes "x > 0"
shows "x ≥ 0"
sorry

```
(Note that I am new to Isabelle, so there might be better ways of doing this.)
```
```
I would be interested in some built-in rule, or a theory in the library, that would simply do this inference for me.
```
```
I am less interested in writing my own proof of this in place of the "sorry" above, as my overall formalisation is a higher-level applied one.
```
Cheers, and thanks in advance for any help,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Building & Exploring Web Based Environments.  Seville, Spain, 27 Jan–
1 Feb 2013.  Deadline 2 Sep.  http://iaria.org/conferences2013/WEB13.html

```

• Follow-Ups:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.