Added a new contrib div_and_mod and few modifs here and there.

[helm.git] / helm / matita / library / Z / z.ma

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 11dd836f667b6ed884753f80ec88ac86e731e8d7..afe80e736030489184d85257a693ecb08316e466 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/".
+set "baseuri" "cic:/matita/Z/z".
 
 include "nat/compare.ma".
 include "nat/minus.ma".
@@ -310,8 +310,8 @@ qed.
 
 
 theorem associative_Zplus: associative Z Zplus.
-change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))).
-(* simplify. *) 
+change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). 
+(* simplify. *)
 intros.elim x.simplify.reflexivity.
 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
 rewrite < (Zpred_Zplus_neg_O y).
@@ -331,7 +331,24 @@ rewrite > Zplus_Zsucc (Zplus (pos e1) y).
 apply eq_f.assumption.
 qed.
 
-variant assoc_Zplus : 
-\forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
+variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
 \def associative_Zplus.
 
+(* Zopp *)
+definition Zopp : Z \to Z \def
+\lambda x:Z. match x with
+[ OZ \Rightarrow OZ
+| (pos n) \Rightarrow (neg n)
+| (neg n) \Rightarrow (pos n) ].
+
+theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
+intro.elim x.
+apply refl_eq.
+simplify.
+rewrite > nat_compare_n_n.
+simplify.apply refl_eq.
+simplify.
+rewrite > nat_compare_n_n.
+simplify.apply refl_eq.
+qed.
+