import proveit
from proveit import defaults
from proveit import B
from proveit.logic import Not
theory = proveit.Theory() # the theorem's theory
%proving to_contraposition
defaults.assumptions = list(to_contraposition.all_conditions()) + [Not(B)]
A_implies_B = defaults.assumptions[0]
A_implies_B.deny_antecedent().as_implication(Not(B))
%qed