proposition: Lemma anddec : forall P Q : Prop, P \/ ~ P -> Q \/ ~ Q -> P /\ Q \/ ~ (P /\ Q).
proof: Proof. intros. elim H. elim H0. left. split. assumption. assumption. right. intro. apply H1. elim H3. intros. assumption. right. intro. apply H1. elim H2. intros. assumption. Qed.
imports: Arith ZArith EqNat