proposition: Theorem Zpower_pos_gt_0 : forall b p, (0 < b)%Z -> (0 < Zpower_pos b p)%Z.
proof: Proof. intros b p Hb. rewrite Zpower_pos_nat. induction (nat_of_P p). easy. rewrite Zpower_nat_S. now apply Zmult_lt_0_compat. Qed.
imports: Coq(ZArith Lia Zquot)