Theorem: HTPI.not_imp_iff_not_and (HTPILib/HTPIDefs.lean)

State before:
p q : Prop
⊢ ¬(q → p) ↔ ¬p ∧ q
Tactic:
rw [not_imp]
State after:
p q : Prop
⊢ q ∧ ¬p ↔ ¬p ∧ q

State before:
p q : Prop
⊢ q ∧ ¬p ↔ ¬p ∧ q
Tactic:
exact And.comm
State after:
no goals