gcd : (x : Nat) -> (y : Nat) -> CmpNat x y -> Nat
gcd aa bb cc = ?gcd_rhs