標準ライブラリの有理数って、Leibniz equalityじゃないから

微妙に使いにくいじゃないですか。ssreflectを読んでたら、こういうのを簡単に Leibniz equality にする方法が分かったので書いてみた。

まず、ZP = Z * positive の上に普通に同値関係を定義する ZP_eq : ZP -> ZP -> Prop。

次に、この同値関係で割ったときの代表元を返す関数を作る。canceled: ZP -> ZP。普通に約分しつくした形を代表元にする。

そして、魔法のような eq_irrelevance を証明する。

最後に ZP の部分集合 { x | canceled x = x } をQとする。これはもちろん代表元全体の集合だ。
仕上げに魔法のように Q_eq_dec を ZP_eq_Q_eq を証明する。