Каким образом?
Мне знакомо понятие математического доказательства. А про информатическое доказательство впервые слышу.
Обычно индуктивно, через сохранение инварианта цикла. Инвариант цикла - это истинное логическое выражение над значениями переменных в коде, которое остаётся истинным при переходе к следующей итерации. Если инвариант цикла сохраняется, он истинный на первом входе в цикл и цикл останавливается, то на выходе из цикла инвариант цикла будет истинным.
У вас
в цикле только возрастает и ограничен сверху, так что, цикл останавливается. Значит, вам нужно доказать, что переменные
и
хранят два последовательных числа Фибоначчи (с уточнением зависимости от
), и что это утверждение истинно на входе в цикл и сохраняет истинность при переходе к следующей итерации цикла, будучи истинным на предыдущей.