How to define gcd using the stdlib?

[simonmasson]

I would like to write a simple Gcd function. It would look like this in python3:

def Gcd(a,b):
    if a == b : 
        return a
    if a > b : 
        return Gcd(a-b, b)
    if a < b : 
        return Gcd(a, b-a)

For now, I cannot do conditions and negation between two integers.

I tried to do this:

module Gcd;
  open import Stdlib.Prelude;
  open import Stdlib.Data.Nat.Ord;

  If : Bool -> ℕ → ℕ → ℕ;
  If true x _ := x;
  If false _ x := x;

  gcd : ℕ → ℕ → ℕ;
  gcd a b :=
    If (a == b)
      a
    (If (a > b)
      (gcd a-b b)
    (gcd a b-a));
end;