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
Could you also include the code giving the error? Could help people understand what's the error is about better.
I want to prove above relation . lt from library may helpful in proving the above relation? Secondly, (destruct <=) gives error.
You should transform your goal before applying
repeat rewrite Bool.andb_true_iff. repeat rewrite Nat.ltb_lt.
Last updated: Jan 31 2023 at 14:03 UTC