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 left_if_not_right
defaults.assumptions = [in_bool(A), in_bool(B), Or(A, B), Not(A), Not(B)]
AorB = Or(A, B)
AorB.affirm_via_contradiction(A) # prove A via contradiction
%qed