Search code examples
coqcoq-tactic

How to destruct a theorem into all three disjuncts in one step?

I have already proved the following lemma:

Lemma ord_semiconnex_bool : forall (alpha beta : ord),
  ord_ltb alpha beta = true \/ ord_ltb beta alpha = true \/ ord_eqb alpha beta = true.

I would like to do case analysis on it for another theorem I'm proving, and I'm trying to apply it to the objects:

gamma1 alpha1 : ord

But if I say:

destruct (ord_semiconnex_bool gamma1 alpha1).

This gives me two branches instead of three. In the first branch I get:

H0 : ord_ltb gamma1 alpha1 = true

And in the second branch I get:

H0 : ord_ltb alpha1 gamma1 = true \/ ord_eqb gamma1 alpha1 = true

So I've just been calling "destruct H0" when I'm in the second branch, giving me the two further sub-branches I want. But that's pretty inelegant and my proofs look pretty ugly as a result.

Is there a way I can destruct my theorem into its 3 disjuncts all at once?

Solution 
  • destruct (...) as [ H1 | [ H2 | H3 ] ]