# Library decidability

# To be or not to be equal

Unfortunately, the previous result in Prop cannot be used
to guide a computation. We turn to sumbool which is analogue
to or but lies in Type.

Can you guess what function underlies your proof?

Define a recursive function find : nat → list nat → bool
such that find n l = true iff n belongs to l.
To compare two natural numbers m and n, you can simply use
if nat_dec m n then .. else ...

The List module comes with the In predicate, which is defined
as a fixpoint over lists, returning a Prop. The module also comes
with results about In, which you can search as shown below, and
which you can reuse directly.

Show that find matches its specification given using In.
Your only option is to proceed by induction over the list.
When if nat_dec a n then .. else .. is visible in the goal,
the tactic destruct (nat_dec m n) will perform case analysis
in a convenient manner, enriching each case with the hypothesis
m=n or m≠n.