proposition: Theorem Zpower_gt_1 : forall p, (0 < p)%Z -> (1 < Zpower r p)%Z.
proof: Proof. intros [|p|p] Hp ; try easy. simpl. rewrite Zpower_pos_nat. generalize (lt_O_nat_of_P p). induction (nat_of_P p). easy. intros _. rewrite Zpower_nat_S. assert (0 < Zpower_nat r n)%Z. clear. induction n. easy. rewrite Zpower_nat_S. apply Zmult_lt_0_compat with (2 := IHn). apply radix_gt_0. apply Z.le_lt_trans with (1 * Zpower_nat r n)%Z. rewrite Zmult_1_l. now apply (Zlt_le_succ 0). apply Zmult_lt_compat_r with (1 := H). apply radix_gt_1. Qed.
imports: Coq(ZArith Lia Zquot)