proposition: Lemma Zpower_pos_1_r x : Z.pow_pos x 1 = x.
proof: Proof. Proof (Z.pow_1_r x). Lemma Zpower_pos_1_l p : Z.pow_pos 1 p = 1. Proof. now apply (Z.pow_1_l (Zpos p)). Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower