proposition: Theorem spec_power_posc x p: [[power_pos x p]] = [[x]] ^ Pos.to_nat p.
proof: Proof. unfold to_Qc. transitivity (Q2Qc ([x]^Zpos p)). unfold Q2Qc. apply Qc_decomp; unfold this. apply Qred_complete; apply spec_power_pos; auto. induction p using Pos.peano_ind. simpl; ring. rewrite Pos2Nat.inj_succ; simpl Qcpower. rewrite <- IHp; clear IHp. unfold Qcmult, Q2Qc. apply Qc_decomp; unfold this. apply Qred_complete. setoid_replace ([x] ^ Zpos (Pos.succ p))%Q with ([x] * [x] ^ Zpos p)%Q. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. simpl. rewrite <- Pos.add_1_l. rewrite Qpower_plus_positive; simpl; apply Qeq_refl. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig