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.