# How can I use a (three terms) decidable axiom in a case analysis?

In Coq, I made some record structure $$I$$ and also make a strict order and equality $$<$$ and $$==$$.

And I showed that $$a < b$$ or $$a == b$$ or $$b < a$$ for every $$a, b \in I$$.

forall a b : I, a < b \/ a == b \/ b < a


Since my construction is not decidable, I use an decidable axiom.

Axiom I_dec : forall a b : I, {a < b} + {a == b} + {b < a}.


I want to use this axiom in case analysis. However, I cannot deal with all three cases.

For example,

Example example :
forall a b : I, if (I_dec a b) then a < b else True.
Proof.
intros. destruct (I_dec a b) as [[H|H]|H].
{ simpl. exact H. }
{ simpl.


I want to reach only the most left case $$a < b$$, however it is impossible for me.

Is there a way to deal with all three cases respectively?

Probably a problem with notations, incompatible with your use of if. Let's have a look at I_dec's structure (I set I = nat).

Unset Printing Notations.
Check I_dec.

I_dec
: forall a b : nat, sumor (sumbool (lt a b) (eq a b)) (lt b a)


The main cases of I_dec a b are (sumbool (lt a b) (eq a b)) and (lt b a).

A possible workaround (among others) is to define a variant of if:

Notation if' t t1 t2 :=
match t with inleft (left H) => t1 | _ => t2 end.

Example example :
forall a b : nat, if' (I_dec a b) (a < b) True.
Proof.
intros; destruct (I_dec a b) as [[H | _] | _]; auto.
Qed.