proposition: Lemma sqrt_var_maj_2: forall h : R, Rabs h <= /2 -> Rabs (sqrt (1 + h) - 1) <= Rabs h / 2 + (Rabs h) * (Rabs h) / 4.
proof: Proof. intros h H1. case (Rle_or_lt 0 h); intros Sh. assert (0 <= h <= 1). apply Rabs_le_inv in H1. lra. rewrite 2!Rabs_pos_eq. apply Rminus_le. interval with (i_autodiff h, i_prec 30). apply Sh. interval with (i_prec 30). assert (-1/2 <= h <= 0). apply Rabs_le_inv in H1. lra. rewrite 2!Rabs_left. apply Rplus_le_reg_l with (h / 2 - h * h / 4). replace (h / 2 - h * h / 4 + - (sqrt (1 + h) - 1)) with ((-h/2) * (-1 + h / 2 + 2 / (sqrt(1 + h) + 1))). apply Rle_trans with (-h/2 * 0%R). 2: right ; field. apply Rmult_le_compat_l. lra. interval with (i_autodiff h, i_prec 30). assert (0 < (sqrt (1 + h) + 1)). interval. replace (sqrt (1 + h) - 1) with (h / (sqrt (1 + h) + 1)). field. interval. apply Rmult_eq_reg_l with (sqrt (1 + h) + 1). 2:apply Rgt_not_eq; assumption. apply trans_eq with h. field. apply Rgt_not_eq; assumption. apply trans_eq with (Rsqr (sqrt (1 + h)) -1). rewrite Rsqr_sqrt. ring. lra. unfold Rsqr; ring. exact Sh. apply Rlt_minus. rewrite <- sqrt_1 at 2. apply sqrt_lt_1_alt. lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)