Я уже доказал следующую лемму:
Lemma ord_semiconnex_bool : forall (alpha beta : ord),
ord_ltb alpha beta = true \/ ord_ltb beta alpha = true \/ ord_eqb alpha beta = true.
Я хотел бы провести анализ случая для нее для другой теоремы, которую я доказываю, и я пытаюсь применить ее к объектам:
gamma1 alpha1 : ord
Но если я скажу:
destruct (ord_semiconnex_bool gamma1 alpha1).
Это даст мне две ветви вместо трех.В первой ветке я получаю:
H0 : ord_ltb gamma1 alpha1 = true
А во второй ветке я получаю:
H0 : ord_ltb alpha1 gamma1 = true \/ ord_eqb gamma1 alpha1 = true
Так что я просто звоню "destruct H0", когда я ввторая ветвь, давая мне две дополнительные ветки, которые я хочу.Но это довольно нелегко, и в результате мои доказательства выглядят довольно некрасиво.
Есть ли способ, которым я могу разложить свою теорему на три дизъюнкта одновременно?