diff options
Diffstat (limited to 'theories/Ints/num/ZnZ.v')
| -rw-r--r-- | theories/Ints/num/ZnZ.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v index ee40989890..1e03170310 100644 --- a/theories/Ints/num/ZnZ.v +++ b/theories/Ints/num/ZnZ.v @@ -168,6 +168,7 @@ Section Spec. spec_of_pos : forall p, Zpos p = (Z_of_N (fst (w_of_pos p)))*wB + [|(snd (w_of_pos p))|]; spec_zdigits : [| w_zdigits |] = Zpos w_digits; + spec_more_than_1_digit: 1 < Zpos w_digits; (* Basic constructors *) spec_0 : [|w0|] = 0; |