proposition: Theorem spec_oppc: forall q, [[opp q]] = -[[q]].
proof: Proof. intros q; unfold Qcopp, to_Qc, Q2Qc. apply Qc_decomp; unfold this. apply Qred_complete. rewrite spec_opp, <- Qred_opp, Qred_correct. apply Qeq_refl. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig