I have a theorem to prove on lean,
theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B)
For which to prove, I guess, I need to use,
or.elim (B ∨ ¬B) (assume b: B, ...) (assume nb:¬B, ...)
For which, again, I have to prove
B v ¬B
So, how do I proceed with this? Is there any better method?