fact: Record almost_ring_theory : Prop := mk_art { ARadd_0_l : forall x, 0 + x == x; ARadd_comm : forall x y, x + y == y + x; ARadd_assoc : forall x y z, x + (y + z) == (x + y) + z; ARmul_1_l : forall x, 1 * x == x; ARmul_0_l : forall x, 0 * x == 0; ARmul_comm : forall x y, x * y == y * x; ARmul_assoc : forall x y z, x * (y * z) == (x * y) * z; ARdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); ARopp_mul_l : forall x y, -(x * y) == -x * y; ARopp_add : forall x y, -(x + y) == -x + -y; ARsub_def : forall x y, x - y == x + -y }.
imports: Setoid Morphisms BinPos BinNat