proposition: Lemma Qccompare_spec (x y : Qc) : CompareSpec (x=y) (x<y) (x>y) (x ?= y).
proof: Proof. now case_eq (x ?= y); constructor; [rewrite Qceq_alt | rewrite Qclt_alt | rewrite Qcgt_alt]. Qed.
imports: QArith_base Qcanon Equalities Orders OrdersTac