proposition: Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]).
proof: Proof. intros [z1 | x1 y1] [z2 | x2 y2]; unfold Qcompare, compare; qsimpl. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig