a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a → ¬b) ∧ (¬b → ¬a) ↔ (b → a) ∧ (a → b)
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a ↔ ¬b) ↔ (a ↔ b)
rw [@iff_def (¬a), @iff_def' a]
no goals
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a → ¬b) ∧ (¬b → ¬a) ↔ (b → a) ∧ (a → b)
exact and_congr not_imp_not not_imp_not