proposition: Theorem Zpower_plus : forall n k1 k2, (0 <= k1)%Z -> (0 <= k2)%Z -> Zpower n (k1 + k2) = (Zpower n k1 * Zpower n k2)%Z.
proof: Proof. intros n k1 k2 H1 H2. now apply Zpower_exp ; apply Z.le_ge. Qed.
imports: Coq(ZArith Lia Zquot)