theorem not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := by simp only
