proposition: Theorem exbefore_ok : forall (P : nat -> Prop) (n : nat), (exists q : nat, q < n /\ P q) <-> exbefore P n.
proof: Proof. intro P. simple induction n. simpl in |- *. split. intros. elim H. intros. elim H0. intros. elim (lt_n_O x). assumption. intros. elim H. intros m IHm. simpl in |- *. elim IHm. intros. split. intro. elim H1. intro. intros. elim H2. intros. elim (le_lt_or_eq x m). intros. left. apply H. split with x. split. assumption. assumption. intros. right. rewrite H5 in H4. assumption. apply (le_S_n x m). assumption. intros. elim H1. intros. case H0. assumption. intros. split with x. elim H3. intros. split. unfold lt in |- *. unfold lt in H4. apply le_S. assumption. assumption. intros. split with m. split. unfold lt in |- *. apply le_n. assumption. Qed.
imports: Arith ZArith EqNat