Decidable.v: One of De Morgan's laws only needs one arg to be decidable

theories/Basics/Decidable.v

@@ -274,16 +274,32 @@ Defined.
 
 (** Various logical laws don't hold constructively as they do classically due to a required use of excluded middle. For us, this means that some laws require further assumptions on the decidability of propositions. *)
 
-(** Here we give the dual De Morgan Law which complements the one given in Iff.v *)
-Definition iff_not_prod A B `{Decidable A} `{Decidable B}
+(** Here we give the dual De Morgan's Law which complements the one given in Iff.v.  One direction requires that one of the two propositions be decidable, while the other direction needs no assumption.  We state the latter property first, to avoid duplication in the proof. *)
+Definition not_prod_sum_not A B : ~ A + ~ B -> ~ (A * B).
+Proof.
+  intros [na|nb] [a b].
+  - exact (na a).
+  - exact (nb b).
+Defined.
+
+Definition iff_not_prod 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).
-  - intros [na|nb] [a b].
-    + exact (na a).
-    + exact (nb b).
+  - apply not_prod_sum_not.
+Defined.
+
+Definition 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.

theories/Basics/Iff.v

@@ -43,7 +43,7 @@ Coercion iff_equiv {A B : Type} (f : A <~> B)
 
 (** ** Logical Laws *)
 
-(** De Morgan Law, the dual statement about negating a product appears in Decidable.v due to decidability requirements. *)
+(** One of De Morgan's Laws.  The dual statement about negating a product appears in Decidable.v due to decidability requirements. *)
 Definition iff_not_sum A B : ~ (A + B) <-> ~ A * ~ B.
 Proof.
   split.