proposition: Fact ex11 x y : x * x = y * y <-> Rabs x = Rabs y.
proof: Proof. split; intros H. assert (H1: (x - y) * (x + y) = 0). transitivity (x * x - y * y); [ring|lra]. split_Rabs; destruct (Rmult_integral _ _ H1) as [H2 | H2]; lra. replace x with (--x); [idtac|ring]. replace y with (--y); [idtac|ring]. split_Rabs; rewrite H; ring. Qed.
imports: Reals Psatz