У ядра нет правила «не меньше»: та же мысль, записанная через «не больше», доказывается

(длина результат) не меньше 1 — сетка примеров. 1 не больше (длина результат) — доказано. Тело, подпись и смысл при этом те же: в IEEE-754 a ≥ b и b ≤ a истинны и ложны на одних и тех же входах, включая «не число» (ложны обе) и пару 0/−0 (истинны обе).

Причина в наборе правил. Решающих правил у ядра пять — «не меньше 0», «не больше конечного литерала», «не больше терма», «равно», «содержит», — и только первое говорит про «не меньше», да и то в единственном частном случае «с нулём». Всё остальное «не меньше» вида у цели не имеет вовсе и получает отказ «у цели этого случая нет вида, к которому у ядра есть правило».

Чем подтверждено. Прогон по всем двадцати модулям flang/stdlib: каждое A не меньше B (кроме не меньше 0) заменено на B не больше A, ведомость пересчитана. Закрывается три утверждения — dictionary «Положить» («после записи словарь непуст»), hashmap «Вписать» («после вписывания список звеньев непуст») и utf8 «Байты кодовой точки» («байтов у точки хотя бы один»). Остальные перевороты не меняют вердикта. Ветка u/dokazat-bibl над 09d71d4d.

Что из этого следует автору. Писать границу снизу как «литерал не больше терма», а не как «терм не меньше литерала». Это не подгонка под ядро: обе записи означают ровно одно, а доказывается одна.

Что из этого следует языку. Правило «не меньше» — зеркало правила «не больше», и завести его дешевле, чем объяснять авторам, какой стороной писать неравенство.

Связано: a-conjunction-goal-is-beyond-the-kernel-but-costs-only-six-claims