proposition: Theorem alldec : forall (P : nat -> Prop) (N : nat), (forall n : nat, P n \/ ~ P n) -> (forall x : nat, x < N -> P x) \/ ~ (forall x : nat, x < N -> P x).
proof: Proof. intro P. simple induction N. left. intros. elim (lt_n_O x). assumption. intros M IH decP. elim IH. elim (decP M). left. intros. unfold lt in H1. elim (le_lt_or_eq x M). intros. apply H0. assumption. intros. rewrite H2. assumption. apply le_S_n. assumption. right. intro. apply H. apply H1. apply lt_n_Sn. right. intro. apply H. intros. apply H0. apply lt_S. assumption. assumption. Qed.
imports: Arith ZArith EqNat