Take something like the least upper bound property of the reals. Suppose I assume this axiom, suitably expressed in Coq’s logic, i.e. forall S subset of reals, if S is non-empty and exists x such that x is an upper bound on S, then there exists z such that z is an upper bound and if a is also an upper bound, a >= z."

So this means I can create a function, called supremum, from S to least upper bound of S. In Coq, given an axiom / assumption / theorem like that, how can I then use it to create a function, presumably a FixedPoint? Supremum is just an example, in many places in math we say “given S there exists unique x such that…”, and this let’s you talk about a function of S. How do I do that in Coq? Another example in the sqrt() function for any positive real.