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 ?

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.

Doesn't `rewrite ltr1n`

work?

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 !

Maybe a problem with the new Search command in 8.12 ? This worked for me `Search _ (1 < _) (_ < _)%N.`

, but I am still using `ssrsearch`

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

Last updated: Feb 05 2023 at 06:28 UTC