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