История изменений

Исправление SZT, 26.03.16 08:44 (текущая версия) :

Вот тебе на alt-ergo

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

Исходная версия SZT, 26.03.16 08:44:

Вот тебе на alt-ergo

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