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
Last updated: Sep 23 2023 at 08:01 UTC