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



On Fri, Aug 10, 2012 at 8:35 AM, Christoph LANGE <c.lange at cs.bham.ac.uk> wrote:
> 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"

by (rule less_imp_le)

- Brian





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