Я изо всех сил пытаюсь найти тактику или переписать правила для Coq, чтобы применить хорошо известные свойства равенств и неравенств, такие как: преобразование H: a < b в H: a + c < b + c или преобразование a = b в a + c = b + c.
Каждый раз, когда мне приходится доказывать очевидные вещи, связанные с арифметикой, это обычно сводится к хаотическому c связке cut и подробным объяснениям самых базовых c фактов, что далеко от читабельности чего я хочу добиться.
Есть ли способы сделать это немного менее многословным?