From 9c8bb7e7c2548d2f37e5387cdce45df2b8fc9b43 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 15 Jul 2005 11:44:14 +0000
Subject: [PATCH] Added a new contrib div_and_mod and few modifs here and
 there.

---
 helm/matita/library/Z/z.ma                    | 27 +++++++++++++++----
 .../library/higher_order_defs/relations.ma    |  3 +++
 helm/matita/library/logic/connectives.ma      |  8 +++---
 helm/matita/library/nat/orders.ma             |  3 ---
 helm/matita/library/nat/orders_op.ma          |  2 +-
 helm/matita/library/nat/plus.ma               |  1 -
 6 files changed, 30 insertions(+), 14 deletions(-)

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 11dd836f6..afe80e736 100644
--- 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 ff75c9d95..a2aa625a7 100644
--- 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 835bb6873..a5aab65f5 100644
--- 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 1939b3c13..b8e92fa2b 100644
--- 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 801e123d2..32a58115d 100644
--- 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 fbb3fcc90..e8750d0cb 100644
--- 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 
-- 
2.39.2