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: Sep 23 2023 at 08:01 UTC