proposition: Theorem spec_power_norm : forall x z, [power_norm x z] == [x]^z.
proof: Proof. destruct z. simpl; nzsimpl; red; auto. apply spec_power_pos. simpl. rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig