@Paolo Giarrusso thanks for the feedback :smile:
In case someone else (new to this) comes accross a similar problem here is the rest:
Next Obligation.
destruct n as [|n'].
- discriminate.
- apply (Nat.div_lt _ 256) ; lia.
Qed.
Nikola Katić has marked this topic as resolved.
After adding decreasing fuel
argument, everything was straightforward... Closing this topic :check:
Nikola Katić has marked this topic as resolved.
Last updated: Jan 27 2023 at 02:04 UTC