Question: I want to make a function of natural numbers comparison in coq 
I declare a Set of invariant contain sup, inf, egal 

```
Inductive invr:Type:=inf | sup | egal.

```

And I define a function comparaison

```
Definition comparaison (inv:invr)(a b:nat):bool:=
  match invr with
  |inf => if (a < b) then true else false  
  |sup => if (a > b) then true else false 
  |egal=> if (a = b) then true else false 
  end. 

```

But it does not work! Thanks for your response.

Answer: 
You are trying to match type (set) invr with its constructors values instead of variable inv, so you get an error 

> 
> The term "invr" has type "Set" while it is expected to have type 
>  "invr".
> 
> 
> 

You need to do the matching for `inv`, not `invr`

```
Definition comparaison (inv:invr)(a b:nat):bool:=
  match inv with
  |inf => if (a < b) then true else false  
  |sup => if (a > b) then true else false 
  |egal=> if (a = b) then true else false 
  end. 

```

Also make sure that you have <, >, = notations are defined to return bool, because by default they return `Prop`, which can't be used in if/else. So you need to use beq\_nat, and leb from Arith.

Simplified final version (removed redundant if/else branches).

```
Require Import Coq.Arith.Arith.

Inductive invr : Type:= inf | sup | egal.

Definition comparaison (inv:invr)(a b:nat):bool:=
  match inv with
  |inf => leb a b
  |sup => leb b a
  |egal=> beq_nat a b
  end. 

```
This is a typical beginner mistake.

`<` stands for `lt`, which has type:

```
lt : nat -> nat -> Prop

```

That is, `a < b` is just a proposition, not a procedure that computes whether `a` is less than `b`!
The same goes for equality.

What you want to use is a function that computes the truth of these propositions, either as a boolean or as a richer type:

In the library `Arith`:

```
beq_nat: nat -> nat -> bool
leb: nat -> nat -> bool

(* or the more informative versions which return proofs of what they decide *)
eq_nat_dec: forall n m : nat, {n = m} + {n <> m}
lt_dec: forall n m : nat, {n < m} + {~ n < m}

```

So the following is a valid expression:

```
if beq_nat a b then true else false

```

Also note that the following is a valid expression equivalent to the precedent one (since `beq_nat` returns a `bool`):

```
beq_nat a b

```