diff options
Diffstat (limited to 'flocq/Core/FLX.v')
| -rw-r--r-- | flocq/Core/FLX.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v index 803d96ef..78bffba5 100644 --- a/flocq/Core/FLX.v +++ b/flocq/Core/FLX.v @@ -48,7 +48,7 @@ Proof. intros k. unfold FLX_exp. generalize prec_gt_0. -repeat split ; intros ; omega. +repeat split ; intros ; lia. Qed. Theorem FIX_format_FLX : @@ -212,7 +212,7 @@ Proof. case (negligible_exp_spec FLX_exp). intros _; reflexivity. intros n H2; contradict H2. -unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. +unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; lia. Qed. Theorem generic_format_FLX_1 : @@ -221,13 +221,13 @@ Proof. unfold generic_format, scaled_mantissa, cexp, F2R; simpl. rewrite Rmult_1_l, (mag_unique beta 1 1). { unfold FLX_exp. - rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. - rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. + rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. + rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. rewrite <- bpow_plus. now replace (_ + _)%Z with Z0 by ring. } rewrite Rabs_R1; simpl; split; [now right|]. unfold Z.pow_pos; simpl; rewrite Zmult_1_r; apply IZR_lt. -assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); omega. +assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); lia. Qed. Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. @@ -356,7 +356,7 @@ destruct NE_prop as [H|H]. now left. right. unfold FLX_exp. -split ; omega. +split ; lia. Qed. End RND_FLX. |