aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Lt.v
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-03-10 17:46:01 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-03-10 17:46:01 +0000
commit9f8ccadf2f68ff44ee81d782b6881b9cc3c04c4b (patch)
treecb38ff6db4ade84d47f9788ae7bc821767abf638 /theories/Arith/Lt.v
parent20b4a46e9956537a0bb21c5eacf2539dee95cb67 (diff)
mise sous CVS du repertoire theories/Arith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Lt.v')
-rwxr-xr-xtheories/Arith/Lt.v151
1 files changed, 151 insertions, 0 deletions
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
new file mode 100755
index 000000000..4c5167e82
--- /dev/null
+++ b/theories/Arith/Lt.v
@@ -0,0 +1,151 @@
+
+(* $Id$ *)
+
+Require Le.
+
+Theorem lt_n_Sn : (n:nat)(lt n (S n)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_n_Sn : arith v62.
+
+Theorem lt_S : (n,m:nat)(lt n m)->(lt n (S m)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_S : arith v62.
+
+Theorem lt_n_S : (n,m:nat)(lt n m)->(lt (S n) (S m)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_n_S : arith v62.
+
+Theorem lt_S_n : (n,m:nat)(lt (S n) (S m))->(lt n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_S_n : arith v62.
+
+Theorem lt_O_Sn : (n:nat)(lt O (S n)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_O_Sn : arith v62.
+
+Theorem lt_n_O : (n:nat)~(lt n O).
+Proof le_Sn_O.
+Hints Resolve lt_n_O : arith v62.
+
+Theorem lt_n_n : (n:nat)~(lt n n).
+Proof le_Sn_n.
+Hints Resolve lt_n_n : arith v62.
+
+Lemma S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Lemma lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)).
+Proof.
+Induction 1; Simpl; Auto with arith.
+Qed.
+Hints Immediate lt_pred : arith v62.
+
+Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n).
+Destruct 1; Simpl; Auto with arith.
+Save.
+Hints Resolve lt_pred_n_n : arith v62.
+
+(* Relationship between le and lt *)
+
+Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_le_S : arith v62.
+
+Theorem lt_n_Sm_le : (n,m:nat)(lt n (S m))->(le n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_n_Sm_le : arith v62.
+
+Theorem le_lt_n_Sm : (n,m:nat)(le n m)->(lt n (S m)).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate le_lt_n_Sm : arith v62.
+
+Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_le_weak : arith v62.
+
+Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).
+Proof.
+Induction n; Auto with arith.
+Intros; Absurd O=O; Trivial with arith.
+Qed.
+Hints Immediate neq_O_lt : arith v62.
+
+Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+Hints Immediate lt_O_neq : arith v62.
+
+(* Transitivity properties *)
+
+Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p).
+Proof.
+Induction 2; Auto with arith.
+Qed.
+
+Theorem lt_le_trans : (n,m,p:nat)(lt n m)->(le m p)->(lt n p).
+Proof.
+Induction 2; Auto with arith.
+Qed.
+
+Theorem le_lt_trans : (n,m,p:nat)(le n m)->(lt m p)->(lt n p).
+Proof.
+Induction 2; Auto with arith.
+Qed.
+
+Hints Resolve lt_trans lt_le_trans le_lt_trans : arith v62.
+
+Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
+Proof.
+Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n).
+Proof.
+Red; Intros n m Lt Le; Exact (le_not_lt m n Le Lt).
+Qed.
+Hints Immediate le_not_lt lt_not_le : arith v62.
+
+Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem nat_total_order: (m,n: nat) ~ m = n -> (lt m n) \/ (lt n m).
+Proof.
+Intros m n diff.
+Elim (le_or_lt n m); [Intro H'0 | Auto with arith].
+Elim (le_lt_or_eq n m); Auto with arith.
+Intro H'; Elim diff; Auto with arith.
+Qed.