proposition: Theorem decDeMorgan : forall (N : nat) (P : nat -> Prop), (forall n : nat, P n \/ ~ P n) -> ((exists x : nat, x < N /\ P x) <-> ~ (forall x : nat, x < N -> ~ P x)).
proof: Proof. split. intro. elim H0. intros. intro. elim H1. intros. apply (H2 x H3 H4). elim N. intros. elim H0. intros. elim (lt_n_O x). assumption. intros M IH. intros. elim (H M). intros. split with M. split. apply lt_n_Sn. assumption. intros. cut (~ (forall x : nat, x < M -> ~ P x)). intros. elim IH. intros. split with x. elim H3. intros. split. apply lt_S. assumption. assumption. assumption. intro. apply H0. intros. elim (le_lt_or_eq x M). intros. apply H2. assumption. intros. rewrite H4. assumption. unfold lt in H3. apply le_S_n. assumption. Qed.
imports: Arith ZArith EqNat