Stream: Coq users

Topic: less than relation

view this post on Zulip sara lee (Aug 05 2022 at 17:42):

b < S (list_max [b] + k

while b & k are nat. Above is correct statement ,auto with arith should solve it (either k is zero or not).But it does not work.

view this post on Zulip sara lee (Aug 05 2022 at 17:42):

(deleted)

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

You should simplify your goal with cbn, then auto with arithshould work.
You can also use the lia tactic (you must Require Import Lia before).

view this post on Zulip sara lee (Aug 05 2022 at 18:29):

Ok,thanks.

Last updated: Oct 01 2023 at 19:01 UTC