Specializations of basic logic lemmas

These are useful for omega while constructing proofs, but not considered generally useful so are hidden in the Lean.Omega namespace.

If you find yourself needing them elsewhere, please move them first to another file.

theorem Lean.Omega.and_not_not_of_not_or {p : Prop} {q : Prop} (h : ¬(p ∨ q)) : ¬p ∧ ¬q

theorem Lean.Omega.Decidable.or_not_not_of_not_and {p : Prop} {q : Prop} [Decidable p] [Decidable q] (h : ¬(p ∧ q)) : ¬p ∨ ¬q

theorem Lean.Omega.Decidable.and_or_not_and_not_of_iff {p : Prop} {q : Prop} [Decidable q] (h : p ↔ q) : p ∧ q ∨ ¬p ∧ ¬q

theorem Lean.Omega.Decidable.not_iff_iff_and_not_or_not_and {a : Prop} {b : Prop} [Decidable a] [Decidable b] : ¬(a ↔ b) ↔ a ∧ ¬b ∨ ¬a ∧ b

theorem Lean.Omega.Decidable.and_not_or_not_and_of_not_iff {a : Prop} {b : Prop} [Decidable a] [Decidable b] (h : ¬(a ↔ b)) : a ∧ ¬b ∨ ¬a ∧ b

theorem Lean.Omega.Decidable.and_not_of_not_imp {a : Prop} {b : Prop} [Decidable a] (h : ¬(a → b)) : a ∧ ¬b

theorem Lean.Omega.ite_disjunction {α : Type u} {P : Prop} [Decidable P] {a : α} {b : α} : P ∧ (if P then a else b) = a ∨ ¬P ∧ (if P then a else b) = b