Stream: Coq users

Topic: invert IZR

view this post on Zulip Dubravka Kutlesic (Oct 13 2021 at 14:30):

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.

view this post on Zulip Guillaume Melquiond (Oct 13 2021 at 14:33):

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

Last updated: Sep 23 2023 at 08:01 UTC