diff --git a/susp_product.hlean b/susp_product.hlean
new file mode 100644
index 0000000..3de39d6
--- /dev/null
+++ b/susp_product.hlean
@@ -0,0 +1,5 @@
+import core
+open susp smash pointed wedge prod
+
+definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ (X ∧ Y)) :=
+  sorry