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
<=?) compute by destructing
b, following the pattern-matching in the definition of
Last updated: Feb 01 2023 at 11:04 UTC