I'm trying to prove such theorem without any success for now. Can someone help or give a hint?

```
Require Import Reals.
Open Scope R.
Theorem Rsqrt_of_square (x: R) (H: 0 <= x * x): Rsqrt (mknonnegreal (x * x) H) = Rabs x.
Proof.
Admitted.
```

I replaced Rsqrt with sqrt, had to rewrite a bit but it's solution.

Lessness has marked this topic as resolved.

Looking at what `Search Rsqrt.`

gives. You can use `Rsqrt_Rsqrt`

by applying first `Rsqr_inj`

.

Thank you!

Last updated: Jun 25 2024 at 15:02 UTC