雑談

なぜか無い補題

Coqのライブラリにはなぜか無い補題というものがある。 例えばZmult_le_reg_rというレンマはZArithのZorderライブラリにあるが、 これの左バージョンは無いのだ。 ちなみにZmult_le_reg_rとは次のような内容である。 Zmult_le_reg_r : forall n m p:Z, p > 0…