proposition: Theorem Zpower_gt_0 : forall p, (0 <= p)%Z -> (0 < Zpower r p)%Z.
proof: Proof. intros p Hp. rewrite Zpower_Zpower_nat with (1 := Hp). induction (Z.abs_nat p). easy. rewrite Zpower_nat_S. apply Zmult_lt_0_compat with (2 := IHn). apply radix_gt_0. Qed.
imports: Coq(ZArith Lia Zquot)