Inequalities and coercions

Stream: new members

[Donald Sebastian Leung]

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]

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]

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]

The lemma name might have the word cast in rather thancoe , I never worked out the difference

[Donald Sebastian Leung]

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: