proposition: Theorem strong_spec_opp: forall q, [opp q] = -[q].
proof: Proof. intros [z | x y]; simpl. rewrite ZZ.spec_opp; auto. match goal with |- context[NN.eqb ?X ?Y] => generalize (NN.spec_eqb X Y); case NN.eqb end; auto; rewrite NN.spec_0. rewrite ZZ.spec_opp; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig