proposition: Theorem spec_comparec: forall q1 q2, compare q1 q2 = ([[q1]] ?= [[q2]]).
proof: Proof. unfold Qccompare, to_Qc. intros q1 q2; rewrite spec_compare; simpl; auto. apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig