import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import in_bool, Not, Or
from proveit.logic.booleans.implication import affirm_via_contradiction
theory = proveit.Theory() # the theorem's theory
%proving right_if_not_left
defaults.assumptions = [in_bool(A), in_bool(B), Or(A, B), Not(A), Not(B)]
AorB = Or(A, B)
AorB.affirm_via_contradiction(B)
%qed