proposition: Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n.
proof: Proof. assert (F0: forall x, (-x)^2 = x^2). intros x; rewrite Z.pow_2_r; ring. unfold pow_pos, to_Z; intros [x | x] [p | p |]; try rewrite NN.spec_pow_pos; try ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. rewrite Pos2Z.inj_xI; repeat rewrite Zpower_exp; auto with zarith. repeat rewrite Z.pow_mul_r; auto with zarith. rewrite F0; ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. rewrite Pos2Z.inj_xO; repeat rewrite Zpower_exp; auto with zarith. repeat rewrite Z.pow_mul_r; auto with zarith. rewrite F0; ring. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig