proposition: Lemma spec_norm_denum : forall n d, [norm_denum n d] == [Qq n d].
proof: Proof. unfold norm_denum; intros; simpl; qsimpl. congruence. nsubst; auto with zarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig