Stream: Coq users

Topic: help from library

view this post on Zulip sara lee (Aug 27 2022 at 16:18):

Which lemma from standard libray may be helpful in the following condition

(a1 + 1 <=? b) && k1<=k2 && k3<=k4
(a1 - 1 <=? b) && k1<=k2 && k3<=k4

view this post on Zulip Julin S (Aug 29 2022 at 03:55):

Could you also include the code giving the error? Could help people understand what's the error is about better.

view this post on Zulip sara lee (Aug 30 2022 at 15:13):

I want to prove above relation . lt from library may helpful in proving the above relation? Secondly, (destruct <=) gives error.

view this post on Zulip Pierre Castéran (Aug 30 2022 at 18:44):

You should transform your goal before applying Nat.ltb_lt.

repeat rewrite Bool.andb_true_iff.  repeat rewrite Nat.ltb_lt.

Last updated: Jan 31 2023 at 14:03 UTC