I am currently working with Coq and I am encountering a problem that I don't know how to solve.

Let's say we are working with a given type, I'll take `nat` for the example, and I want to use a function `f` that might fail. To compensate the failure, we define `f` to be of type `nat -> option nat`.

Now I have a given hypothesis `H: nat -> bool` under which f doesn't fail, and I have even proved the lemma

```
Lemma no_error_in_f : forall (n:nat), H n = true -> exists (u:nat), f n = Some u.

```

I want to define a function `g: nat->nat` which gives the result of `f` on `n` if `H n` is satisfied, and just gives `n` otherwise. This function should be well defined, but I don't know how to define it properly.
If I try something naive like
`Definition g (n:nat) := if H n then f n else n.`, there is a problem in the typing system.

Does anyone knows how to gather all the elements and tell the system that the definition is legal?