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: Jun 16 2024 at 03:41 UTC