# Re: [ProofPower] Real Numbers - Proofs

```Artur,

```
You may like to know that there is a so-called "component" proof context called 'z_reals which will make evaluation of real arithmetic expressions happen automatically when you rewrite.

```
Try:

set_merge_pcs["'z_reals", "z_library"];
set_goal([], %SZT% real 30 %mem% real 20 ..%down%R real 40 %>%);
a(rewrite_tac[z_%bbR%_dot_dot_def]);

Regards,

Rob.

Artur Oliveira Gomes wrote:
```
```Hi there

Now I know how to prove it: using z_R_<=_conv.

Thanks anyway,

Artur

```
2009/3/25 Artur Oliveira Gomes <artur.o.go...@gmail.com <mailto:artur.o.go...@gmail.com>>
```
Hi there,

How could I prove that given two real numbers, 20 and 30, that 20 <=40?
Moreover, given three real numbers, 20, 30 and 40,
how could I prove that 30 <in> 20..40.

Regards,

```
-- Artur Oliveira Gomes
```

--
Artur Oliveira Gomes

------------------------------------------------------------------------

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
```
```

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
```