ᛒ
Почему я умею гуглить, а ты нит
у тя талант
Size: a a a
2021 March 05
Oℕ
короч антон говорит
Oℕ
что оно автоматически получается
Oℕ
т.к. неравенство вычислимое
Oℕ
Oℕ
ничё делать не надо
AT
но, да, док-ва будут отличаться
Oℕ
но, да, док-ва будут отличаться
ну done то найдёт его
Oℕ
я уже забыл, честно говоря даже синтаксис
Oℕ
но я так понимаю, что done, by ... и какой-то // смогут сами это решить
Oℕ
потому что n <=? n автоматически в true вычислится
w
потому что n <=? n автоматически в true вычислится
хахаха, да мне вообще похуй
AT
потому что n <=? n автоматически в true вычислится
Не, в общем случае не вычислится. Нужна индукция
AT
Но конструкторы редукцией удалятся.
Oℕ
а что-то вроде by apply: le_n сработает?
AT
а что-то вроде by apply: le_n сработает?
должно, но это будет уже читинг)
AT
а, погоди, я скорее неформально прочитал твой вопрос