# Non-trivial existence proof in type theory

What are some examples of existence proofs in Coq/Agda etc., where the constructed natural number is useful from mathematical point of view, but it's non-obvious from the proof what it should be? I am aware of the Brunerie number in homotopical versions of type theory, but as far as I know, this doesn't really compute or takes far too long in current implementations of Cubical Type Theory. Are there any interesting applications in Agda/Coq etc. with K, which compute and weren't done by hand on paper? Are there any interesting numbers in Cubical Agda, which were computed?