blob: 8c7c1f809cea1e55d20cf56d248476169c6950ca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
Require Export BigN.
Require Import ZMake.
Module BigZ := Make BigN.
Definition bigZ := BigZ.t.
Delimit Scope bigZ_scope with bigZ.
Bind Scope bigZ_scope with bigZ.
Bind Scope bigZ_scope with BigZ.t.
Bind Scope bigZ_scope with BigZ.t_.
Notation " i + j " := (BigZ.add i j) : bigZ_scope.
Notation " i - j " := (BigZ.sub i j) : bigZ_scope.
Notation " i * j " := (BigZ.mul i j) : bigZ_scope.
Notation " i / j " := (BigZ.div i j) : bigZ_scope.
Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope.
Theorem spec_to_Z:
forall n, BigN.to_Z (BigZ.to_N n) =
(Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z.
intros n; 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.
Qed.
Theorem spec_to_N n:
(BigZ.to_Z n =
Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z.
intros n; 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.
Qed.
Theorem spec_to_Z_pos:
forall n, (0 <= BigZ.to_Z n ->
BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z.
intros n; 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.
Qed.
|
