proposition: Lemma resolution : forall x y : R, x >= 0 -> y >= 0 -> x * x = y * y -> x = y.
proof: Proof. intros. rewrite <- (def_sqrt x); auto with real. rewrite <- (def_sqrt y); auto with real. rewrite <- sqrt_mult; auto with real. rewrite <- sqrt_mult; auto with real. Qed.