I seem to be unable to prove simply
1 < 2 in a
realFieldType and need to write
rewrite -[X in X < 2]addr0 /(1 + 1) ler_lt_add //=. What is the short way to do that ? Am I missing a lemma ?
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?
by rewrite ltr_addl ltr01. is already better, thanks.
rewrite ltr1n work?
Cyril Cohen said:
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 !
Maybe a problem with the new Search command in 8.12 ? This worked for me
Search _ (1 < _) (_ < _)%N. , but I am still using
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