proposition: Lemma Rext: ring_eq_ext add mul opp _==_.
proof: Proof. constructor; solve_proper. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia