prove the naturals have no zero divisors

HigherOrderCO · Oct 19, 2021 · 436b11d · 436b11d
1 parent 013e480
commit 436b11d
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/base/Nat/mul/equal_zero.kind b/base/Nat/mul/equal_zero.kind
@@ -0,0 +1,16 @@
+Nat.mul.equal_zero(
+  n: Nat, m: Nat
+  Hyp: Equal<Nat>(Nat.mul(n, m), 0)
+): Or<Equal<Nat>(n, 0), Equal<Nat>(m, 0)>
+  case n with Hyp {
+    zero:
+      left(refl)
+    succ:
+      case m with Hyp {
+        zero:
+          right(refl)
+        succ:
+          let contra = Nat.succ_neq_zero!(Hyp)
+          Empty.absurd!(contra)
+      }!
+  }!