we restored the scripts of \lambda\delta version 1

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / base_blt.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/base_blt.v b/helm/coq-contribs/LAMBDA-TYPES/base_blt.v
deleted file mode 100644 (file)
index ae00365..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/base_blt.v
+++ /dev/null
@@ -1,33 +0,0 @@
-Require Arith.
-Require base_tactics.
-Require base_hints.
-
-(*#* #stop file *)
-
-      Fixpoint blt [m,n: nat] : bool := Cases n m of
-         | (0) m       => false
-         | (S n) (0)   => true
-         | (S n) (S m) => (blt m n)
-      end.
-
-   Section blt_props. (******************************************************)
-
-      Theorem lt_blt: (x,y:?) (lt y x) -> (blt y x) = true.
-      XElim x; [ Intros; Inversion H | XElim y; Simpl; XAuto ].
-      Qed.
-
-      Theorem le_bge: (x,y:?) (le x y) -> (blt y x) = false.
-      XElim x; [ XAuto | XElim y; Intros; [ Inversion H0 | Simpl; XAuto ] ].
-      Qed.
-
-      Theorem blt_lt: (x,y:?) (blt y x) = true -> (lt y x).
-      XElim x; [ Intros; Inversion H | XElim y; Simpl; XAuto ].
-      Qed.
-
-      Theorem bge_le: (x,y:?) (blt y x) = false -> (le x y).
-      XElim x; [ XAuto | XElim y; Intros; [ Inversion H0 | Simpl; XAuto ] ].
-      Qed.
-
-   End blt_props.
-
-      Hints Resolve lt_blt le_bge : ltlc.