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.
You should simplify your goal with
auto with arithshould work.
You can also use the
lia tactic (you must
Require Import Lia before).
Last updated: Oct 01 2023 at 19:01 UTC