A B `{Decidable A} : ~ (A * B) <-> ~ A + ~ B. Proof. split. - intros np. destruct (dec A) as [a|na]. + exact (inr (fun b => np (a, b))). + exact (inl na). - apply not_prod_sum_not. Defined.
Require Import