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

[helm.git] / helm / matita / library / higher_order_defs / relations.ma

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