proposition: Theorem spec_mul : forall x y, [mul x y] == [x] * [y].
proof: Proof. intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl. rewrite Pos.mul_1_r, Z2Pos.id; auto. rewrite Z.mul_eq_0 in *; intuition lia. nsubst; auto with zarith. nsubst; auto with zarith. nsubst; nzsimpl; auto with zarith. rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig