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

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.
+

diff --git a/helm/matita/library/higher_order_defs/relations.ma b/helm/matita/library/higher_order_defs/relations.ma
index ff75c9d9569cbd277eaaa500f4eac4eb0f833e73..a2aa625a733e57491ad852b7f837374535291f25 100644 (file)
--- a/helm/matita/library/higher_order_defs/relations.ma
+++ b/helm/matita/library/higher_order_defs/relations.ma
@@ -28,3 +28,6 @@ definition transitive: \forall A:Type.\forall R:A \to A \to Prop.Prop
 \def 
 \lambda A.\lambda R.\forall x,y,z:A.R x y \to R y z \to R x z.
 
+definition irreflexive: \forall A:Type.\forall R:A \to A \to Prop.Prop
+\def 
+\lambda A.\lambda R.\forall x:A.Not (R x x).
\ No newline at end of file

diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 835bb68734c397f2ae6bdbc1e6ef5ed0a1b22e18..a5aab65f5d16fb77eda84a18be88e163802a86d2 100644 (file)
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/connectives/".
+set "baseuri" "cic:/matita/logic/connectives/".
 
 inductive True: Prop \def
 I : True.
 
-default "true" cic:/matita/logic/True.ind.
+default "true" cic:/matita/logic/connectives/True.ind.
 
 inductive False: Prop \def .
 
-default "false" cic:/matita/logic/False.ind.
+default "false" cic:/matita/logic/connectives/False.ind.
 
 definition Not: Prop \to Prop \def
 \lambda A. (A \to False).
@@ -30,7 +30,7 @@ theorem absurd : \forall A,C:Prop. A \to Not A \to C.
 intros. elim (H1 H).
 qed.
 
-default "absurd" cic:/matita/logic/absurd.ind.
+default "absurd" cic:/matita/logic/connectives/absurd.con.
 
 inductive And (A,B:Prop) : Prop \def
     conj : A \to B \to (And A B).

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 1939b3c13764e4c9937dbe5af73a3bd09abb0dc2..b8e92fa2b6987f34cfecbf81841bee405d10ca0a 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -14,9 +14,6 @@
 
 set "baseuri" "cic:/matita/nat/orders".
 
-include "logic/connectives.ma".
-include "logic/equality.ma".
-include "nat/nat.ma".
 include "nat/plus.ma".
 include "higher_order_defs/ordering.ma".
 

diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma
index 801e123d2c901a65c7894c04fe71c9e5920700f6..32a58115dab3dececccbc1eb98fcf9ea431f1ad4 100644 (file)
--- a/helm/matita/library/nat/orders_op.ma
+++ b/helm/matita/library/nat/orders_op.ma
@@ -90,7 +90,7 @@ apply le_times_l.assumption.
 apply le_times_r.assumption.
 qed.
 
-theorem le_n_nm: \forall n,m:nat.le (S O) n \to le m (times n m).
+theorem le_times_n: \forall n,m:nat.le (S O) n \to le m (times n m).
 intros.elim H.simplify.
 elim (plus_n_O ?).apply le_n.
 simplify.rewrite < sym_plus.apply le_plus_n.

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index fbb3fcc90b76e4ceb7b037336f3393336ccffea3..e8750d0cba0f41a0995a23524a8d6f887a83204e 100644 (file)
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -14,7 +14,6 @@
 
 set "baseuri" "cic:/matita/nat/plus".
 
-include "logic/equality.ma".
 include "nat/nat.ma".
 
 let rec plus n m \def