proposition: Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
proof: Proof. constructor. intros. red. rewrite BigN.spec_pow, BigN.spec_of_N. rewrite Zpower_theory.(rpow_pow_N). destruct n; simpl. reflexivity. induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto. Qed.
imports: Lia CyclicAxioms Ring63 NSig NSigNAxioms NMake NProperties GenericMinMax