proposition: Lemma Rsqrt_sqr : forall x (y : nonnegreal), 0 <= x -> (x ^ 2 = y)%R -> Rsqrt y = x.
proof: Proof. intros x y x_pos Heq ; unfold Rsqrt. destruct (Rsqrt_exists y (cond_nonneg y)) as [z [z_pos Hz]]. apply Rsqr_inj ; try assumption. symmetry ; rewrite pow2_sqr, Heq ; apply Hz. Qed.
imports: Reals MyRIneq Fourier Lia Lra Rsequence_usual_facts