# Zulip Chat Archive

## Stream: new members

### Topic: Inequalities and coercions

#### Donald Sebastian Leung (Feb 29 2020 at 03:59):

In the standard library, there is a lemma `int.coe_nat_le_coe_nat_of_le`

which states that one can coerce both sides of an inequality involving natural numbers to get an inequality involving integers. Is there a similar lemma which performs lifting from the natural numbers to the reals?

#### Kevin Buzzard (Feb 29 2020 at 08:09):

There is probably one which works for maps from the naturals to arbitrary totally ordered semirings or something, and you might be able to find it with `library_search`

if you just copy the statement of the lemma above and replace the ints with reals. The reason ints are treated differently is some consequences of a design decision, something about the canonical map from the naturals to the integers being a constructor.

#### Kevin Buzzard (Feb 29 2020 at 08:11):

I should also say that the whole point of tactics like `norm_cast`

is to enable the user to not have to ask questions like this. Your question reminds me of the old days

#### Kevin Buzzard (Feb 29 2020 at 08:12):

The lemma name might have the word `cast`

in rather than`coe`

, I never worked out the difference

#### Donald Sebastian Leung (Feb 29 2020 at 08:56):

Kevin Buzzard said:

I should also say that the whole point of tactics like

`norm_cast`

is to enable the user to not have to ask questions like this. Your question reminds me of the old days

Thanks, using `norm_cast`

made my life much easier :stuck_out_tongue:

Last updated: Dec 20 2023 at 11:08 UTC