proposition: Lemma Rsqrt_exists : forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }.
proof: Proof. intros. set (f := fun x:R => Rsqr x - y). assert (f 0 <= 0). { unfold f; rewrite Rsqr_0. unfold Rminus; rewrite Rplus_0_l. apply Rge_le. apply Ropp_0_le_ge_contravar; assumption. } assert (continuity f). { replace f with (Rsqr - fct_cte y)%F by reflexivity. apply continuity_minus;apply derivable_continuous. - apply derivable_Rsqr. - apply derivable_const. } destruct (total_order_T y 1) as [[Hlt| -> ]|Hgt]. - assert (0 <= f 1). { unfold f. rewrite Rsqr_1. apply Rplus_le_reg_l with y. rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; left; assumption. } assert (f 0 * f 1 <= 0). { rewrite Rmult_comm; pattern 0 at 2; rewrite <- (Rmult_0_r (f 1)). apply Rmult_le_compat_l; assumption. } assert (X := IVT_cor f 0 1 H1 (Rlt_le _ _ Rlt_0_1) H3). elim X; intros t H4. exists t. elim H4; intros. split. + elim H5; intros; assumption. + unfold f in H6. symmetry; apply Rminus_diag_uniq; exact H6. - exists 1. split. + left; apply Rlt_0_1. + symmetry; apply Rsqr_1. - assert (0 <= f y). { unfold f. apply Rplus_le_reg_l with y. rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r. pattern y at 1; rewrite <- Rmult_1_r. unfold Rsqr; apply Rmult_le_compat_l. - assumption. - left; exact Hgt. } assert (f 0 * f y <= 0). { rewrite Rmult_comm; pattern 0 at 2; rewrite <- (Rmult_0_r (f y)). apply Rmult_le_compat_l; assumption. } assert (X := IVT_cor f 0 y H1 H H3). elim X; intros t H4. exists t. elim H4; intros. split. + elim H5; intros; assumption. + unfold f in H6. symmetry; apply Rminus_diag_uniq; exact H6. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra