The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Lucian M. Patcas wrote:
> Say f is
>
> f (t : nat) := if t>1 and t<2000 then True else False
>
> How can I prove this
>
> forall t : nat, t >=2 -> t <= 1000 -> f t

Require Import Omega.

Definition f (t : nat) := IF t > 1 /\ t < 2000 then True else False.

Goal forall t : nat, t >=2 -> t <= 1000 -> f t.
  unfold f, IF_then_else; intuition omega.
Qed.