proposition: Lemma Qcompare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x ?= y).
proof: Proof. unfold Qeq, Qlt, Qcompare. case Z.compare_spec; now constructor. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool