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

Question

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?

Answer 1

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.