proposition: Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p.
proof: Proof. intros [ z | n d ] p; unfold power_pos. simpl. rewrite ZZ.spec_pow_pos, Qpower_decomp. red; simpl; f_equal. now rewrite Pos2Z.inj_pow, Z.pow_1_l. simpl. rewrite ZZ.spec_pow_pos. destr_eqb; nzsimpl; intros. - apply Qeq_sym; apply Qpower_positive_0. - rewrite NN.spec_pow_pos in *. assert (0 < NN.to_Z d ^ Zpos p)%Z by (apply Z.pow_pos_nonneg; auto with zarith). lia. - exfalso. rewrite NN.spec_pow_pos in *. nsubst. rewrite Z.pow_0_l' in *; [lia|discriminate]. - rewrite Qpower_decomp. red; simpl; do 3 f_equal. apply Pos2Z.inj. rewrite Pos2Z.inj_pow. rewrite 2 Z2Pos.id by (generalize (NN.spec_pos d); lia). now rewrite NN.spec_pow_pos. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig