@@ -91,6 +91,12 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
9191-- Comparisons
9292--------------------------------------------------------------------------------
9393
94+||| Proofs that `n` or `m` is not equal to Z
95+data NotBothZero : (n, m : Nat) -> Type where
96+ LeftIsNotZero : NotBothZero (S n) m
97+ RightIsNotZero : NotBothZero n (S m)
98+
99+
94100||| Proofs that `n` is less than or equal to `m`
95101||| @ n the smaller number
96102||| @ m the larger number
@@ -386,16 +392,15 @@ log2 (S n) = log2NZ (S n) SIsNotZ
386392--------------------------------------------------------------------------------
387393-- GCD and LCM
388394--------------------------------------------------------------------------------
389−partial
390−gcd : Nat -> Nat -> Nat
391−gcd a Z = a
392−gcd a b = assert_total (gcd b (a `modNat` b))
395+gcd : (a: Nat) -> (b: Nat) -> .{auto ok: NotBothZero a b} -> Nat
396+gcd a Z = a
397+gcd Z b = b
398+gcd a (S b) = assert_total $ gcd (S b) (modNatNZ a (S b) SIsNotZ)
393399
394−partial
395400lcm : Nat -> Nat -> Nat
396−lcm _ Z = Z
397−lcm Z _ = Z
398−lcm x y = divNat (x * y) (gcd x y)
401+lcm _ Z = Z
402+lcm Z _ = Z
403+lcm a (S b) = assert_total $ divNat (a * (S b)) (gcd a (S b))
399404
400405
401406--------------------------------------------------------------------------------