Add inhabited_prod.

Lebesgue/Subset.v

@@ -1633,6 +1633,12 @@ Section Prod_Facts.
 
 Context {U1 U2 : Type}. (* Universes. *)
 
+Lemma inhabited_prod :
+  inhabited U1 -> inhabited U2 -> inhabited (U1 * U2).
+Proof.
+intros [x1] [x2]; apply (inhabits (x1, x2)).
+Qed.
+
 Lemma prod_emptyset_l :
   forall A2, prod emptyset A2 = @emptyset (U1 * U2).
 Proof.