diff options
Diffstat (limited to 'flocq/Core/Fcore_Raux.v')
| -rw-r--r-- | flocq/Core/Fcore_Raux.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v index d728e0ba..939002cf 100644 --- a/flocq/Core/Fcore_Raux.v +++ b/flocq/Core/Fcore_Raux.v @@ -1673,7 +1673,7 @@ Qed. (** Another well-used function for having the logarithm of a real number x to the base #β# *) Record ln_beta_prop x := { ln_beta_val :> Z ; - _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R + _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R }. Definition ln_beta : |