Более формальный вывод из доказательства по принципу наименьшего числа?
Когда доказывают какой-то факт, используя принцип наименьшего числа, то заканчивают доказательство, получив противоречие, найдя ещё меньше элемент (чем i-й, когда предположение было, что i-й элемент на самом деле является наименьше)
Вроде бы звучит естественно и логично сделать вывод, что такого элемента i нет и вроде бы все привыкли к таким рассуждениям
Но, если упарываться формализмом, разве в этом доказательстве нету следующей прощенной части: если для i-го элемента (который предполагался наименьшим) был найден i-1, являющий тоже "наименьшим", то (для любого начального j) можно пройтись таким окном из начиная с j и итерируясь по (k, k-1) (уменьшая k) каждый раз находя всё новый и новый "наименьший" элемент, и дойти до базы, которая точно не является наименьшим. ?
Ну и получается то же самое домино, что и в индукции только в другую сторону