proposition: Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow.
proof: Proof. constructor. intros. unfold BigZ.eq, BigZ_of_N. rewrite BigZ.spec_pow, BigZ.spec_of_Z. rewrite Zpower_theory.(rpow_pow_N). destruct n; simpl. reflexivity. induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto. Qed.
imports: BigN ZProperties ZDivFloor ZSig ZSigZAxioms ZMake Ring Lia