proposition: Theorem spec_mulc x y: [[mul x y]] = [[x]] * [[y]].
proof: Proof. unfold to_Qc. transitivity (Q2Qc ([x] * [y])). unfold Q2Qc. apply Qc_decomp; unfold this. apply Qred_complete; apply spec_mul; auto. unfold Qcmult, Q2Qc. apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig