proposition: Theorem Zpower_nat_S : forall b e, Zpower_nat b (S e) = (b * Zpower_nat b e)%Z.
proof: Proof. intros b e. rewrite (Zpower_nat_is_exp 1 e). apply (f_equal (fun x => x * _)%Z). apply Zmult_1_r. Qed.
imports: Coq(ZArith Lia Zquot)