GCD

write a function that, given natural numbers a and b, computes their greatest common denominator.

Function Signature

def GCD(a b:Nat):Nat

Theorem Signature

theorem gcd_is_div (x y: Nat):
  (p: x > 0)→ ((GCD x y) ∣ x) ∧ ((GCD x y) ∣ y)

Additional Theorem Signature

theorem gcd_is_greatest (x y: Nat):
  (x>0) → Not (∃ z: Nat, z∣ x ∧ z∣ y ∧ z> GCD x y )

View All Submissions

Please log in or register to submit a solution for this challenge.