proposition: Theorem spec_div x y: [div x y] == [x] / [y].
proof: Proof. unfold div; rewrite spec_mul; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig