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 ec0fa89bff..60a836d416 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -746,7 +746,7 @@ Module Make (W0:CyclicType) <: NType. Theorem spec_sqrt: forall x, [sqrt x] = Zsqrt [x]. Proof. intros x. - symmetry. apply Z.sqrt_unique. apply spec_pos. + symmetry. apply Z.sqrt_unique. rewrite <- ! Zpower_2. apply spec_sqrt_aux. Qed. |