proposition: Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q.
proof: Proof. intros(x,y); destruct y; simpl; rewrite ?ZZ.spec_of_Z; auto; destr_eqb; now rewrite ?NN.spec_0, ?NN.spec_of_N. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig