Stream: Coq users

Topic: ✔ How to prove that Rsqrt of squared x is Rabs x?

Lessness (Oct 17 2021 at 16:19):

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.

Lessness (Oct 17 2021 at 16:39):

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

Notification Bot (Oct 17 2021 at 16:39):

Lessness has marked this topic as resolved.

Laurent Théry (Oct 17 2021 at 16:42):

Looking at what Search Rsqrt. gives. You can use Rsqrt_Rsqrt by applying first Rsqr_inj.

Lessness (Oct 17 2021 at 17:00):

Thank you!

Last updated: Sep 23 2023 at 08:01 UTC