I want to use `Coq.QArith`

to compute something. Here is my code: <https://gist.github.com/kindaro/92a7d53a4c9a4297417310dcf0a599b7>. I cannot destruct or eliminate the proof of existence of the number I want to have computed. What do?

use `{ (x: ℚ) | e₂ = Root 2 x}`

instead of `∃ (x: ℚ), e₂ = Root 2 x`

It works, thanks! Why does one work but not the other?

https://coq.inria.fr/doc/language/core/inductive.html#the-match-with-end-construction

in particular the paragraph about Prop

Last updated: Jan 29 2023 at 06:02 UTC