proposition: Theorem Rcompare_sqr : forall x y, Rcompare (x * x) (y * y) = Rcompare (Rabs x) (Rabs y).
proof: Proof. intros x y. destruct (Rcompare_spec (Rabs x) (Rabs y)) as [H|H|H]. apply Rcompare_Lt. now apply Rsqr_lt_abs_1. change (Rcompare (Rsqr x) (Rsqr y) = Eq). rewrite Rsqr_abs, H, (Rsqr_abs y). now apply Rcompare_Eq. apply Rcompare_Gt. now apply Rsqr_lt_abs_1. Qed.
imports: Coq(Psatz Reals ZArith) Zaux