proposition: Theorem Zpower_Zpower_nat : forall b e, (0 <= e)%Z -> Zpower b e = Zpower_nat b (Z.abs_nat e).
proof: Proof. intros b [|e|e] He. apply refl_equal. apply Zpower_pos_nat. elim He. apply refl_equal. Qed.
imports: Coq(ZArith Lia Zquot)