From 96f921b40ded4defb9a93b26e29c058b1fcb4b43 Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sat, 8 Apr 2017 19:39:03 +0200
Subject: [PATCH] b is actually a prime

---
 discrete_log.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/discrete_log.txt b/discrete_log.txt
index 08e5964..30b5143 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -52,7 +52,7 @@ proc IntegerRoot(a:nat): nat
 proc DiscreteLog(p:prime,g:nat,a:nat): res
    requires 1 < p ∧ isPrime(p) ∧ // p is a prime greater than 1
             1 < g ∧ g < p ∧ 
-            ∀b:nat. (0 < b ∧ b < p-1) ⇒ (g^b % p ≠ 1) ∧  g^(p-1)%p = 1 ∧ // g has order p-1
+            ∀b:prime. (0 < b ∧ b < p-1) ⇒ (g^b % p ≠ 1) ∧  g^(p-1)%p = 1 ∧ // g has order p-1
             0 < a ∧ a < p; // a is in ℤ/pℤ - {0}
    ensures (g^result)%p = a;
 {
-- 
2.1.4