import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.negation import negation_contradiction
from proveit.logic import FALSE, Not, Equals
#from proveit.logic.booleans import from_not_false
#from proveit.logic.booleans.implication import modus_tollens_affirmation
theory = proveit.Theory() # the theorem's theory
%proving modus_tollens_denial
defaults.assumptions = modus_tollens_denial.all_conditions()
# Prove Not(A) via the contradition, under the assumptions,
# of B and Not(B) simultaneously being true when A is true.
Not(B).deny_via_contradiction(A)
%qed