proposition: Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
proof: Proof. Proof (mk_art 0 1 radd rmul rsub ropp req (Radd_0_l Rth) (Radd_comm Rth) (Radd_assoc Rth) (Rmul_1_l Rth) Rmul_0_l (Rmul_comm Rth) (Rmul_assoc Rth) (Rdistr_l Rth) Ropp_mul_l Ropp_add (Rsub_def Rth)). Variable C : Type. Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C). Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool). Variable phi : C -> R. Infix "+!" := cadd. Infix "*!" := cmul. Infix "-!" := csub. Notation "-! x" := (copp x). Notation "?=!" := ceqb. Notation "[ x ]" := (phi x). Variable Csth : Equivalence ceq. Variable Ceqe : ring_eq_ext cadd cmul copp ceq. Add Parametric Relation : C ceq reflexivity proved by (@Equivalence_Reflexive _ _ Csth) symmetry proved by (@Equivalence_Symmetric _ _ Csth) transitivity proved by (@Equivalence_Transitive _ _ Csth) as C_setoid. Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext. Proof. exact (Radd_ext Ceqe). Qed.
imports: Setoid Morphisms BinPos BinNat