proposition: Lemma iffdec : forall P Q : Prop, P \/ ~ P -> Q \/ ~ Q -> (P <-> Q) \/ ~ (P <-> Q).
proof: Proof. unfold iff in |- *. intros. apply anddec. apply impdec. assumption. assumption. apply impdec. assumption. assumption. Qed.
imports: Arith ZArith EqNat