Is there a way to "and" two decision procedures into one in Coq?

Question

I am trying to define a function in Coq with a if ... then ... else ... and in my condition for 'if' I would like to test if a nat is in a interval.

For instance a, b, x are nat and I want to test if x is in the interval [a,b], so I would like to have a condition like if (le_gt_dec a x)/\(lt_dec x b) then ... else ... but this doesn't work because the type wanted by the '/\' is Prop on both side and le_gt_dec is not Prop. So I get the error : The term "le_gt_dec a x" has type "{a <= x} + {a > x}" while it is expected to have type "Prop"

I also tried if (le_gt_dec a x)&&(lt_dec x b) then ... else ... but this doesn't work neither.

The only solution I have found for now is to do an if...then...else... inside another if...then...else... so for the function IsIn that I gave as an example it would be :

if (le_gt_dec a x) then ( if (le_gt_dec x b) then ... else ... ) else ...

But by defining functions with this technique it gets very complicated later on when I need to prove stuff on these functions because it makes many cases, so I was wondering if anyone had a better way to define such functions ?

Answer 1

You are probably searching for this:

Require Import Coq.Arith.Arith.

Definition IsIn (a:nat) (b:nat) (x:nat) : bool :=
  andb (leb a x) (leb x b).

Answer 2

Just to expand on @thoferon's answer: Coq let's you add your own syntactic sugar, so you can write

Notation "A && B" := (andb A B). 
Notation "A || B" := (orb  A B).

And then

Eval compute in (if true && false then 1 else 0).
    = 0 : nat
Eval compute in (if true || false then 1 else 0).
    = 1 : nat