Demonstrations for the theory of proveit.logic.booleans.quantification.existence

import proveit
%begin demonstrations

from proveit import a, b
from proveit.logic import Exists, Equals
from proveit.numbers import Add, two, three, five, NaturalPos

eval_2p3 = Add(two, three).evaluation()

eval_2p3:  ⊢  

Exists((a, b), Equals(Add(a, b), five)).conclude_via_example((two, three))

 ⊢  

Exists((a, b), Equals(Add(a, b), five), domain=NaturalPos).conclude_via_example((two, three))

 ⊢  

%end demonstrations