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