diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ/ZMake.v')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index fb760bdf5..f9490cc9c 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -31,6 +31,7 @@ Module Make (N:NType) <: ZType. Definition zero := Pos N.zero. Definition one := Pos N.one. + Definition two := Pos N.two. Definition minus_one := Neg N.one. Definition of_Z x := @@ -64,6 +65,10 @@ Module Make (N:NType) <: ZType. exact N.spec_1. Qed. + Theorem spec_2: to_Z two = 2. + exact N.spec_2. + Qed. + Theorem spec_m1: to_Z minus_one = -1. simpl; rewrite N.spec_1; auto. Qed. |