## 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 thancoe , 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: May 16 2021 at 21:11 UTC