proposition: Theorem allbefore_ok : forall (P : nat -> Prop) (n : nat), (forall q : nat, q < n -> P q) <-> allbefore P n.
proof: Proof. intro. simple induction n. simpl in |- *. split. tauto. intros. elim (lt_n_O q). assumption. simpl in |- *. intros m IHm. elim IHm. intros. split. intros. split. apply H. intros. apply (H1 q). unfold lt in |- *. unfold lt in H2. apply le_S. assumption. apply (H1 m). unfold lt in |- *. apply le_n. intro. elim H1. intro. intro. intros. elim (le_lt_or_eq q m). intros. apply H0. assumption. assumption. intros. rewrite H5. assumption. unfold lt in H4. apply (le_S_n q m). assumption. Qed.
imports: Arith ZArith EqNat