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
InSet(InSet(x, Natural), Boolean).prove()
InSet(InSet(x, NaturalPos), Boolean).prove()
greater_eq(x, zero).prove(assumptions=[InSet(x, Natural)])
greater(x, zero).prove(assumptions=[InSet(x, NaturalPos)])
InSet(x, Natural).prove(assumptions=[InSet(x, NaturalPos)])
%end demonstrations