proposition: Lemma spec_max : forall n m, [max n m] == Qmax [n] [m].
proof: Proof. unfold max, Qmax, GenericMinMax.gmax. intros. rewrite spec_compare; destruct Qcompare; auto with qarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig