Zulip Chat Archive

Stream: new members

Topic: Comparing natural numbers as reals


view this post on Zulip Matei Mandache (Jan 15 2021 at 15:49):

Is there a simple way to compare two natural numbers as reals? In particular, suppose n and m are naturals and we have
h: n ≤ m
is there a way to prove
(n : ℝ) ≤ (m : ℝ)

view this post on Zulip Riccardo Brasca (Jan 15 2021 at 15:51):

nat.cast_le works

view this post on Zulip Johan Commelin (Jan 15 2021 at 15:51):

norm_cast can do that

view this post on Zulip Riccardo Brasca (Jan 15 2021 at 15:53):

I found it with library_search, that for these small lemmas works very well

view this post on Zulip Matei Mandache (Jan 15 2021 at 15:53):

Thank you!

view this post on Zulip Riccardo Brasca (Jan 15 2021 at 15:55):

also assumption_mod_cast does it


Last updated: May 08 2021 at 19:11 UTC