# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: positive reals

#### Damiano Testa (Apr 15 2021 at 06:54):

Dear All,

do strictly positive reals appear in mathlib? If so, are they an `ordered_comm_group`

?

I searched a bit and could not find them.

Thanks!

#### Kevin Buzzard (Apr 15 2021 at 06:56):

Maybe `units nnreal`

is the closest we have -- assuming nnreal is a monoid...

#### Damiano Testa (Apr 15 2021 at 06:57):

Hmm, I can try. I was playing with the inequalities that Johan suggested in `liquid`

and there are very few lemmas about divisibility that apply to `R>0`

since it does not have many instances...

#### Damiano Testa (Apr 15 2021 at 06:57):

Let see if using `units nnreal`

makes it easier!

#### Damiano Testa (Apr 15 2021 at 07:08):

Ok, this works:

```
instance : ordered_comm_group (units ℝ≥0) := by apply_instance
```

#### Kevin Buzzard (Apr 15 2021 at 07:10):

If that's the route you want to go down then probably the next thing to do is to define a constructor which takes in a real and a proof that it's positive, and gives you an element of the units.

#### Damiano Testa (Apr 15 2021 at 07:15):

Since it seems that the lemma that I will use most often is `a / b ≤ a / c ↔ c ≤ b`

, with `a b c : nnreal`

, I will just prove this by breaking up the terms and reducing to the real case. Hopefully, I will not need more lemmas!

#### Damiano Testa (Apr 15 2021 at 07:23):

Not too pretty, but this works:

```
lemma preal.div_le_div_left {a b c : ℝ≥0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
a / b ≤ a / c ↔ c ≤ b :=
begin
cases a with a ha,
cases b with b hb,
cases c with c hc,
have a00 : 0 < a := a0,
have b00 : 0 < b := b0,
have c00 : 0 < c := c0,
erw [div_le_div_left a00 b00 c00],
exact iff.rfl,
end
```

#### Rémy Degenne (Apr 15 2021 at 07:31):

```
lemma preal.div_le_div_left {a b c : ℝ≥0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
a / b ≤ a / c ↔ c ≤ b :=
by rw [nnreal.div_le_iff b0.ne.symm, div_mul_eq_mul_div, nnreal.le_div_iff_mul_le c0.ne.symm,
mul_le_mul_left a0]
```

#### Damiano Testa (Apr 15 2021 at 07:34):

Rémy, thank you very much! I had not found the `nnreal.div_le_iff + ...`

lemmas!

#### Johan Commelin (Apr 15 2021 at 07:40):

Damiano Testa said:

Since it seems that the lemma that I will use most often is

`a / b ≤ a / c ↔ c ≤ b`

, with`a b c : nnreal`

, I will just prove this by breaking up the terms and reducing to the real case. Hopefully, I will not need more lemmas!

Doesn't this work in any `linear_ordered_comm_group_with_zero`

?

#### Johan Commelin (Apr 15 2021 at 07:40):

It's probably just a hole in the API

#### Johan Commelin (Apr 15 2021 at 07:40):

Almost every lemma that's proven for `nnreal`

should work in that generality

#### Damiano Testa (Apr 15 2021 at 07:42):

I could not find the lemmas with inequalities for `linear_ordered_comm_group_with_zero`

: the ones that I found were either for `comm_group`

or `field`

. I was not able to find the `with_zero`

version.

#### Johan Commelin (Apr 15 2021 at 07:46):

There are some holes in the API. https://github.com/leanprover-community/mathlib/blob/master/src/algebra/linear_ordered_comm_group_with_zero.lean#L158 seems to be the only lemma about "div".

#### Johan Commelin (Apr 15 2021 at 07:46):

But it's not even about `div`

.

#### Johan Commelin (Apr 15 2021 at 07:46):

But there's enough about `le`

and `inv`

.

#### Damiano Testa (Apr 15 2021 at 07:47):

Johan, thanks for the pointer: I will try to work with what is available, before trying to fill in the holes!

Last updated: May 19 2021 at 03:22 UTC