Hello, I'm COQ beginner and I'm struggling to prove Lemma helper: forall (x y:Z), (IZR x < IZR y)%R -> (x < y)%Z.

This lemma already exists in the standard library. It is called lt_IZR.

lt_IZR

Last updated: Jan 27 2023 at 02:04 UTC