From d7e249dc1bfc2dd04ccf23c57b7ad40f1902568d Mon Sep 17 00:00:00 2001
From: emakarov
Date: Tue, 16 Oct 2007 16:28:17 +0000
Subject: Added transitivity and irreflexivity of <, as well as < -elimination
 for binary positive numbers.

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/NatInt/NZPlusOrder.v | 67 -----------------------------------
 1 file changed, 67 deletions(-)
 delete mode 100644 theories/Numbers/NatInt/NZPlusOrder.v

(limited to 'theories/Numbers/NatInt/NZPlusOrder.v')

diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v
deleted file mode 100644
index 6368fa5578..0000000000
--- a/theories/Numbers/NatInt/NZPlusOrder.v
+++ /dev/null
@@ -1,67 +0,0 @@
-Require Export NZPlus.
-Require Export NZOrder.
-
-Module NZPlusOrderPropFunct
-  (Import NZPlusMod : NZPlusSig)
-  (Import NZOrderMod : NZOrderSig with Module NZBaseMod := NZPlusMod.NZBaseMod).
-
-Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod.
-Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod.
-Open Local Scope NatIntScope.
-
-Theorem NZplus_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
-Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono.
-Qed.
-
-Theorem NZplus_lt_mono_r : forall n m p, n < m <-> n + p < m + p.
-Proof.
-intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l.
-Qed.
-
-Theorem NZplus_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZlt_trans with (m + p);
-[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l].
-Qed.
-
-Theorem NZplus_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
-Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono.
-Qed.
-
-Theorem NZplus_le_mono_r : forall n m p, n <= m <-> n + p <= m + p.
-Proof.
-intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l.
-Qed.
-
-Theorem NZplus_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZle_trans with (m + p);
-[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l].
-Qed.
-
-Theorem NZplus_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZlt_le_trans with (m + p);
-[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l].
-Qed.
-
-Theorem NZplus_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZle_lt_trans with (m + p);
-[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
-Qed.
-
-End NZPlusOrderPropFunct.
-
-- 
cgit v1.2.3