proposition: Lemma R_power_theory : Ring_theory.power_theory ring1 mul _==_ N.to_nat pow.
proof: Proof. apply Ring_theory.mkpow_th. unfold pow. intros. rewrite Nnat.N2Nat.id. reflexivity. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia