Читаю матан, вижу упражнение на доказательство для САМОПРОВЕРКИ. Решаю, решил неправильно/думаю, что решил неправильно. Лезу в ответы. Не нахожу (там ток СЛОЖНЫЕ). Понимаю что автор не рассчитывал, что его книгу будут читать такие имбецилы как я. ВНИМАНИЕ ВОПРОС Если я вкурю Coq (или че там щас модно), я смогу играть в математика? Или это по большей части дроч^Wборьба с типами, чем средство удобн^Wинтерактивного доказательства теорем?