proveit.numbers.numerals.decimals.posnat1
proveit.logic.equality.sub_left_side_into