fact: Record ring_eq_ext : Prop := mk_reqe { Radd_ext : Proper (req ==> req ==> req) radd; Rmul_ext : Proper (req ==> req ==> req) rmul; Ropp_ext : Proper (req ==> req) ropp }.
imports: Setoid Morphisms BinPos BinNat