proposition: Lemma cring_power_theory : @Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication).
proof: Proof. intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool ZArith_base Algebra_syntax Ncring Ncring_initial Ncring_tac InitialRing