Упражнения по теме Леммы, auto-active verification

1. Сформулируйте данное утверждение и докажите при помощи Why3, солверов и методов Флойда.

   1. У любых двух положительных целых чисел однозначно определено частное от деления одного на другое

   2. Для любого целого неотрицательного числа его целочисленный квадратный корень не меньше целочисленного квадратного корня числа, на единицу большего исходного числа.

   3. Для любого целого числа разница между его квадратом и квадратом числа на единицу большего является нечетным числом.

   4. Для любых двух целых чисел разница их кубов делится нацело на их разность.

2. Определите функцию для возведения одного целого неотрицательного числа в степень другого целого неотрицательного числа. Используйте ее для формулирования и доказательства следующих утверждений.

   1. Для любых целых неотрицательных a b c верно соотношение: ab + c = ab ⋅ ac

   2. Для любых целых неотрицательных a b c верно соотношение: ab ⋅ c = (ab)c