我如何在精益中证明这一点？ p ∨ ¬p

问题描述

我有一个关于精益的定理要证明，

theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B)

为了证明，我想，我需要使用，

or.elim (B ∨ ¬B) (assume b: B,...) (assume nb:¬B,...)

为此，我必须再次证明

B v ¬B

那么，我该如何处理呢？有没有更好的方法？

解决方法

p v ¬p 是来自名为 classical.em 的核心库的引理。

,

import tactic

variables (A B : Prop)

theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B) := by tauto!