diff options
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index c0b8074b6..2eb8584c9 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -105,7 +105,7 @@ Qed. Theorem spec_to_N n: ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. Proof. -intros n; case n; simpl; intros p; +case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. intros p1 H1; case H1; auto. intros p1 H1; case H1; auto. |