Method test_nat_succ_pos

tests/test_z3_semantic.py:421–423

(self, kernel)

        assert _try_prove(n >= NatVal(0))

    def test_nat_succ_pos(self, kernel):
        n = Nat("n")
        assert _try_prove(n + NatVal(1) > NatVal(0))


# ===================================================================