From 80b8635f33060e4a925a96bf6dc60e0386c01903 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 16 Sep 2005 11:56:54 +0000 Subject: [PATCH] added notation for nleq, nlgt, ... --- helm/matita/library/Z/orders.ma | 6 ++++++ helm/matita/library/nat/orders.ma | 10 ++++++++++ 2 files changed, 16 insertions(+) diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma index ec1d6fb52..f97c47eba 100644 --- a/helm/matita/library/Z/orders.ma +++ b/helm/matita/library/Z/orders.ma @@ -38,6 +38,9 @@ definition Zle : Z \to Z \to Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y). +(*CSC: the URI must disappear: there is a bug now *) +interpretation "integer 'neither less nor equal to'" 'nleq x y = + (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)). definition Zlt : Z \to Z \to Prop \def \lambda x,y:Z. @@ -60,6 +63,9 @@ definition Zlt : Z \to Z \to Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y). +(*CSC: the URI must disappear: there is a bug now *) +interpretation "integer 'not less than'" 'nless x y = + (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)). theorem irreflexive_Zlt: irreflexive Z Zlt. change with \forall x:Z. x < x \to False. diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index d592ed0af..811706867 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -24,12 +24,19 @@ inductive le (n:nat) : nat \to Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y). +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural 'neither less nor equal to'" 'nleq x y = + (cic:/matita/logic/connectives/Not.con + (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)). definition lt: nat \to nat \to Prop \def \lambda n,m:nat.(S n) \leq m. (*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y). +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural 'not less than'" 'nless x y = + (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)). definition ge: nat \to nat \to Prop \def \lambda n,m:nat.m \leq n. @@ -42,6 +49,9 @@ definition gt: nat \to nat \to Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y). +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural 'not greater than'" 'ngtr x y = + (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)). theorem transitive_le : transitive nat le. simplify.intros.elim H1. -- 2.39.2