proposition: Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.
proof: Proof. intros. apply mk_reqe; solve_proper. Defined.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool ZArith_base Algebra_syntax Ncring Ncring_initial Ncring_tac InitialRing