# Looking for a value in a tree

Consider the following type:
Require Import ZArith.
Inductive Z_btree : Set :=
| Z_leaf : Z_btree
| Z_bnode : Z->Z_btree->Z_btree->Z_btree.

Define a function taking as argument an integer *z*
and a tree *t:Z_btree* and returning `true` iff *t*
has (at least) an occurrence of *z*.
## Hint

Use the function `Zeq_bool` to compare two intergers wrt equality.
formula.
## Solution

This file

Note: this solution contains also an infix notation
for these formulae.

Suggestion: add propositional variables !

Going home

Pierre Castéran