diff --git a/src/Data/IntegralGCD.idr b/src/Data/IntegralGCD.idr
index 0e2d65d..cd1449b 100644
--- a/src/Data/IntegralGCD.idr
+++ b/src/Data/IntegralGCD.idr
@@ -18,7 +18,7 @@ interface (Eq a, Integral a) => IntegralGCD a where
   gcd x y =
     if x == 0 then y
     else if y == 0 then x
-    else assert_total $ gcd y (x `mod` y)
+    else gcd y (assert_smaller y $ x `mod` y)
 
 
 export IntegralGCD Integer where