proposition: Theorem spec_div_norm x y: [div_norm x y] == [x] / [y].
proof: Proof. unfold div_norm; rewrite spec_mul_norm; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv_norm; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig