Stream: Coq users

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


view this post on Zulip 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.

view this post on Zulip Lessness (Oct 17 2021 at 16:39):

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

view this post on Zulip Notification Bot (Oct 17 2021 at 16:39):

Lessness has marked this topic as resolved.

view this post on Zulip 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.

view this post on Zulip Lessness (Oct 17 2021 at 17:00):

Thank you!


Last updated: Jan 28 2023 at 06:30 UTC