proposition: Lemma sqrt_var_maj : forall h:R, Rabs h <= 1 -> Rabs (sqrt (1 + h) - 1) <= Rabs h.
proof: Proof. intros; assert (0 <= 1 + h). { destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt]. + rewrite (Rabs_left h Hlt) in H. apply Rplus_le_reg_l with (- h). rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; exact H. + left; rewrite Heq; rewrite Rplus_0_r; apply Rlt_0_1. + left; apply Rplus_lt_0_compat. * apply Rlt_0_1. * apply Hgt. } apply Rle_trans with (Rabs (sqrt (Rsqr (1 + h)) - 1)). 2:{ rewrite sqrt_Rsqr. - replace (1 + h - 1) with h; [ right; reflexivity | ring ]. - apply H0. } destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt]. - repeat rewrite Rabs_left. + unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)). change (-1) with (-(1)). do 2 rewrite Ropp_plus_distr; rewrite Ropp_involutive; apply Rplus_le_compat_l. apply Ropp_le_contravar; apply sqrt_le_1. * apply Rle_0_sqr. * apply H0. * pattern (1 + h) at 2; rewrite <- Rmult_1_r; unfold Rsqr; apply Rmult_le_compat_l; lra. + apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r. pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1. * apply Rle_0_sqr. * left; apply Rlt_0_1. * pattern 1 at 2; rewrite <- Rsqr_1; apply Rsqr_incrst_1;lra. + apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r. pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1;lra. - rewrite Heq; rewrite Rplus_0_r; rewrite Rsqr_1; rewrite sqrt_1; right; reflexivity. - repeat rewrite Rabs_right. + unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)); apply Rplus_le_compat_l. apply sqrt_le_1. * apply H0. * apply Rle_0_sqr. * pattern (1 + h) at 1; rewrite <- Rmult_1_r; unfold Rsqr; apply Rmult_le_compat_l;lra. + apply Rle_ge; apply Rplus_le_reg_l with 1. rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r. pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_le_1. * left; apply Rlt_0_1. * apply Rle_0_sqr. * pattern 1 at 1; rewrite <- Rsqr_1; apply Rsqr_incr_1;lra. + apply Rle_ge; left; apply Rplus_lt_reg_l with 1. rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r. pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_lt_1;lra. Qed.
imports: Rbase Rfunctions Ranalysis1 R_sqrt Lra