Stream: math-comp analysis

Topic: 1<2


view this post on Zulip Marie Kerjean (Oct 08 2020 at 18:47):

I seem to be unable to prove simply 1 < 2 in a realFieldType and need to write rewrite -[X in X < 2]addr0 [2]/(1 + 1) ler_lt_add //=. What is the short way to do that ? Am I missing a lemma ?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2020 at 21:37):

Hi @Marie Kerjean , I guess you can avoid the matching using a different lemma, so by rewrite ltr_addl ltr01. for example.

Or would you like 1 < 2 to hold by reflexivity?

view this post on Zulip Marie Kerjean (Oct 09 2020 at 06:37):

by rewrite ltr_addl ltr01. is already better, thanks.

view this post on Zulip Cyril Cohen (Oct 09 2020 at 11:55):

Doesn't rewrite ltr1n work?

view this post on Zulip Marie Kerjean (Oct 09 2020 at 15:23):

Cyril Cohen said:

Doesn't rewrite ltr1n work?

This is what I was looking for. I wasn't able to find it through Search though as I was looking for a "nat" in the name and a more general inequility m < n. Thanks !

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2020 at 15:26):

Maybe a problem with the new Search command in 8.12 ? This worked for me Search _ (1 < _) (_ < _)%N. , but I am still using ssrsearch

view this post on Zulip Marie Kerjean (Oct 09 2020 at 16:26):

Indeed, but I did not search for a specific lemma involving 1. That's my fault.


Last updated: Aug 11 2022 at 01:03 UTC