Require NPeano.
Import NPeano.Nat.
Require Import ExtLib.Tactics.Consider.
Require Import Coq.Bool.Bool.
Require Import ExtLib.Data.Nat.

Require Import Coq.ZArith.ZArith.

Set Implicit Arguments.
Set Strict Implicit.

(**  Some tests *)
Section test.
  Goal forall x y z,  (ltb x y && ltb y z) = true ->
                 ltb x z = true.
(* Goal: forall (x y z : nat) (_ : @Logic.eq bool (andb (ltb x y) (ltb y z)) true), @Logic.eq bool (ltb x z) true *)
  intros x y z.
(* Goal: forall _ : @Logic.eq bool (andb (ltb x y) (ltb y z)) true, @Logic.eq bool (ltb x z) true *)
  consider (ltb x y && ltb y z).
(* Goal: forall _ : and (Peano.lt x y) (Peano.lt y z), @Logic.eq bool (ltb x z) true *)
  consider (ltb x z); auto. intros. exfalso. omega.
  Qed.

  Goal forall x y z,
    ltb x y = true ->
    ltb y z = true ->
    ltb x z = true.
  Proof.
(* Goal: forall (x y z : nat) (_ : @Logic.eq bool (ltb x y) true) (_ : @Logic.eq bool (ltb y z) true), @Logic.eq bool (ltb x z) true *)
    intros. consider (ltb x y); consider (ltb y z); consider (ltb x z); intros; auto.
(* Goal: False *)
    exfalso; omega.
  Qed.

End test.
