I am proving , a <=? b = true (forall a b :nat). I am destructing leb, but i get message " Use Bool.le ". When i use this then again get error .

Do you mean to say that you have an *assumption* of the form `(a <=? b) = true`

? Indeed, such an assumption is likely to be difficult to work with as-is, and you may want to convert it into an `a <= b`

by applying `leb_complete`

. Alternatively, you could make the `leb`

(`<=?`

) compute by destructing `a`

and `b`

, following the pattern-matching in the definition of `leb`

.

Last updated: Feb 01 2023 at 11:04 UTC