Demonstrations for the theory of proveit.numbers.number_sets.natural_numbers

In [1]:
import proveit
from proveit import x
from proveit.logic import Boolean, NotEquals, InSet
from proveit.numbers import zero, greater, greater_eq, Less, LessEq
from proveit.numbers import Natural, NaturalPos
%begin demonstrations

Number set membership demonstrations

In [2]:
InSet(InSet(x, Natural), Boolean).prove()
In [3]:
InSet(InSet(x, NaturalPos), Boolean).prove()
In [4]:
greater_eq(x, zero).prove(assumptions=[InSet(x, Natural)])
In [5]:
greater(x, zero).prove(assumptions=[InSet(x, NaturalPos)])
In [6]:
InSet(x, Natural).prove(assumptions=[InSet(x, NaturalPos)])
In [7]:
%end demonstrations