proposition: Theorem spec_oppc_bis : forall q : Qc, [opp (of_Qc q)] = - q.
proof: Proof. intros. rewrite <- strong_spec_opp_norm by apply strong_spec_of_Qc_bis. rewrite strong_spec_red. symmetry; apply (Qred_complete (-q)%Q). rewrite spec_opp, strong_spec_of_Qc; auto with qarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig