Thanks!

That made it work:

```
Definition isLsbSet {n:nat} (v: Bvector n): bool.
Proof.
refine (
match n as m return m <= n -> bool with
| O => fun _ => false (* There is no LSB *)
| S n' => fun pf => nth_order v (_:n'<n)
end _); trivial.
Show Proof.
Defined.
```

Julin Shaji has marked this topic as resolved.

Last updated: Jun 13 2024 at 19:02 UTC