Исправление SZT, (текущая версия) :
Вот тебе на alt-ergo
goal inf_proff:
forall x : int.
x >= 1 -> (* все натуральные числа больше либо равны 1 *)
(x+1 >= 1) (* всякое натуральное число, если к нему прибавить 1, будет натуральным *)
Исходная версия SZT, :
Вот тебе на alt-ergo
goal inf_proff:
forall x : int.
x >= 1 -> (* все натуральные числа больше либо равны 1 *)
(x >= 1) and (x+1 >= 1) (* всякое натуральное число, если к нему прибавить 1, будет натуральным *)