proposition: Lemma spec_mul_norm_Qz_Qq : forall z n d, [mul_norm_Qz_Qq z n d] == [Qq (ZZ.mul z n) d].
proof: Proof. intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. destr_eqb; nzsimpl; intros Hz. qsimpl; rewrite Hz; auto. destruct Z_le_gt_dec as [LE|GT]. qsimpl. rewrite spec_norm_denum. qsimpl. rewrite Zdiv_gcd_zero in GT; auto with zarith. nsubst. rewrite Zdiv_0_l in *; discriminate. rewrite <- Z.mul_assoc, (Z.mul_comm (ZZ.to_Z n)), Z.mul_assoc. rewrite Zgcd_div_swap0; lia. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig