diff options
| author | letouzey | 2008-06-02 23:26:13 +0000 |
|---|---|---|
| committer | letouzey | 2008-06-02 23:26:13 +0000 |
| commit | f82bfc64fca9fb46136d7aa26c09d64cde0432d2 (patch) | |
| tree | 471a75d813fb70072c384b926f334e27919cf889 /theories/Numbers/Integer/BigZ | |
| parent | b37cc1ad85d2d1ac14abcd896f2939e871705f98 (diff) | |
In abstract parts of theories/Numbers, plus/times becomes add/mul,
for increased consistency with bignums parts
(commit part I: content of files)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/BigZ')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index d2f9b0a024..f547370369 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -80,7 +80,7 @@ Proof. red; intros; zsimpl; auto. Qed. -Lemma plus_opp : forall x : bigZ, x + (- x) == 0. +Lemma add_opp : forall x : bigZ, x + (- x) == 0. Proof. red; intros; zsimpl; auto with zarith. Qed. @@ -91,15 +91,15 @@ Lemma BigZring : ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. Proof. constructor. -exact Zplus_0_l. -exact Zplus_comm. -exact Zplus_assoc. -exact Ztimes_1_l. -exact Ztimes_comm. -exact Ztimes_assoc. -exact Ztimes_plus_distr_r. +exact Zadd_0_l. +exact Zadd_comm. +exact Zadd_assoc. +exact Zmul_1_l. +exact Zmul_comm. +exact Zmul_assoc. +exact Zmul_add_distr_r. exact sub_opp. -exact plus_opp. +exact add_opp. Qed. Add Ring BigZr : BigZring. |