(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require Export bg_hints. 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. (******************************************************) Hints Resolve le_S_n : ld. Lemma lt_blt: (x,y:?) (lt y x) -> (blt y x) = true. Proof. XElim x; [ Intros; Inversion H | XElim y; Simpl; XAuto ]. Qed. Lemma le_bge: (x,y:?) (le x y) -> (blt y x) = false. Proof. XElim x; [ XAuto | XElim y; Intros; [ Inversion H0 | Simpl; XAuto ] ]. Qed. Lemma blt_lt: (x,y:?) (blt y x) = true -> (lt y x). Proof. XElim x; [ Intros; Inversion H | XElim y; Simpl; XAuto ]. Qed. Lemma bge_le: (x,y:?) (blt y x) = false -> (le x y). Proof. XElim x; [ XAuto | XElim y; Intros; [ Inversion H0 | Simpl; XAuto ] ]. Qed. End blt_props. Hints Resolve lt_blt le_bge : ld.