proposition: Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow.
proof: Proof. constructor. intros z n. destruct n as [|p];simpl;trivial. unfold Z.pow_pos. rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1. induction p as [p IHp|p IHp|]; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. Qed.
imports: BinInt Ring_theory