proposition: Lemma cring_almost_ring_theory: almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.
proof: Proof. intros. apply mk_art ;intros. - rewrite ring_add_0_l; reflexivity. - rewrite ring_add_comm; reflexivity. - rewrite ring_add_assoc; reflexivity. - rewrite ring_mul_1_l; reflexivity. - apply ring_mul_0_l. - rewrite cring_mul_comm; reflexivity. - rewrite ring_mul_assoc; reflexivity. - rewrite ring_distr_l; reflexivity. - rewrite ring_opp_mul_l; reflexivity. - apply ring_opp_add. - rewrite ring_sub_def ; reflexivity. Defined.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool ZArith_base Algebra_syntax Ncring Ncring_initial Ncring_tac InitialRing