diff options
Diffstat (limited to 'flocq/Prop')
-rw-r--r-- | flocq/Prop/Div_sqrt_error.v | 4 | ||||
-rw-r--r-- | flocq/Prop/Relative.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/flocq/Prop/Div_sqrt_error.v b/flocq/Prop/Div_sqrt_error.v index 76c7af95..79220438 100644 --- a/flocq/Prop/Div_sqrt_error.v +++ b/flocq/Prop/Div_sqrt_error.v @@ -366,7 +366,7 @@ unfold Rdiv; apply (Rplus_le_reg_r (/ sqrt (1 + 2 * u_ro))); ring_simplify. apply (Rmult_le_reg_r (sqrt (1 + 4 * u_ro) * sqrt (1 + 2 * u_ro))). { apply Rmult_lt_0_compat; apply sqrt_lt_R0; lra. } field_simplify; [|split; apply Rgt_not_eq, Rlt_gt, sqrt_lt_R0; lra]. -unfold Rdiv; rewrite Rinv_1, !Rmult_1_r. +try unfold Rdiv; rewrite ?Rinv_1, ?Rmult_1_r. apply Rsqr_incr_0_var; [|now apply Rmult_le_pos; apply sqrt_pos]. rewrite <-sqrt_mult; [|lra|lra]. rewrite Rsqr_sqrt; [|apply Rmult_le_pos; lra]. @@ -409,7 +409,7 @@ assert (Pu_ro := u_ro_pos beta prec). apply (Rmult_le_reg_r (sqrt (1 + 2 * u_ro) * (1 + u_ro))). { apply Rmult_lt_0_compat; [apply sqrt_lt_R0|]; lra. } field_simplify; [|lra|intro H; apply sqrt_eq_0 in H; lra]. -unfold Rdiv, Rminus; rewrite Rinv_1, !Rmult_1_r, !Rplus_assoc. +try unfold Rdiv; unfold Rminus; rewrite ?Rinv_1, ?Rmult_1_r, !Rplus_assoc. rewrite <-(Rplus_0_r (sqrt _ * _)) at 2; apply Rplus_le_compat_l. apply (Rplus_le_reg_r (1 + u_ro)); ring_simplify. rewrite <-(sqrt_square (_ + 1)); [|lra]; apply sqrt_le_1_alt. diff --git a/flocq/Prop/Relative.v b/flocq/Prop/Relative.v index b936f2f7..5f87bd84 100644 --- a/flocq/Prop/Relative.v +++ b/flocq/Prop/Relative.v @@ -566,7 +566,7 @@ assert (H : (Rabs ((rx - x) / x) <= u_ro / (1 + u_ro))%R). now rewrite (Rabs_Rinv _ Nzx); apply Rinv_le. } apply (Rmult_le_reg_r ((ufpx + Rabs (rx - x)) * (1 + u_ro))). { apply Rmult_lt_0_compat; lra. } - field_simplify; [unfold Rdiv; rewrite Rinv_1, !Rmult_1_r| |]; lra. } + field_simplify; [try unfold Rdiv; rewrite ?Rinv_1, ?Rmult_1_r| |]; lra. } revert H; unfold Rdiv; rewrite Rabs_mult, (Rabs_Rinv _ Nzx); intro H. apply (Rmult_le_reg_r (/ Rabs x)); [now apply Rinv_0_lt_compat, Rabs_pos_lt|]. now apply (Rle_trans _ _ _ H); right; field; split; [apply Rabs_no_R0|lra]. |