proveit.logic.booleans.disjunction.unary_or_reduction
proveit.numbers.numerals.decimals.nat1