Marie Kerjean (Oct 08 2020 at 18:47): 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 ?
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?
Marie Kerjean (Oct 09 2020 at 06:37):by rewrite ltr_addl ltr01. is already better, thanks.
Cyril Cohen (Oct 09 2020 at 11:55):Doesn't rewrite ltr1n work?
Marie Kerjean (Oct 09 2020 at 15:23):Cyril Cohen said:
Doesn't
rewrite ltr1nwork?
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 !
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
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: Apr 19 2024 at 22:01 UTC