Boolean equality over natural numbers in Coq

Question

Is it possible to compare two natural numbers, x and y, in Coq, and have the equality be returned as a boolean value? Ideally I would like to be able to do something like:

Variable x : nat.
Variable y : nat.

if bool_eq x y
  then ...
  else ...

Thanks in advance!

Answer 1

Sure. Coq is very similar to Haskell or OCaml. A function like that is defined in Coq.Arith.EqNat. It's called beq_nat.