In Coq, how do I define a function implicitly, not using Fixedpoint?

For example, define the square root function by f(x)^2 = x.

I looked at the definition of sqrt in std, but it’s a parameter of a module. Do I need a module to define it? I tried:

```
Module Type Foo.
Parameter Inline bubba : nat -> nat.
Axiom bubba_spec: forall a, bubba(a) * bubba(a) = a.
End Foo.
```

But I can neither `Import`

nor `Export Foo`

.

(I get that this definition doesn’t work for the natural numbers, I’m curious what the error message is, also I can fix it up once I get the basic syntax working.)