diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 66b39aca9b..64b8ec844d 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -1244,7 +1244,7 @@ Module Make (W0:CyclicType) <: NType. apply ZnZ.spec_head0; auto with zarith. Qed. - Lemma spec_log2 : forall x, [log2 x] = Zlog2 [x]. + Lemma spec_log2 : forall x, [log2 x] = Z.log2 [x]. Proof. intros. destruct (Z_lt_ge_dec 0 [x]). symmetry. apply Z.log2_unique. apply spec_pos. |