Use assert_smaller instead of assert_total

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