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: Mar 29 2024 at 11:01 UTC