Redundant zero in IsRing #2195
Description
When defining IsRing, zero is provided in the definition. Instead, we can prove zero as its property.
Here is proof of right zero
RightZero : ∀ x → x * 0# ≈ 0#
RightZero x = begin
x * 0# ≈⟨ sym(+-identityʳ _) ⟩
x * 0# + 0# ≈⟨ +-congˡ (sym(-‿inverseʳ x)) ⟩
x * 0# + (x - x) ≈⟨ sym(+-assoc _ _ _) ⟩
(x * 0# + x) - x ≈⟨ +-congʳ (+-congˡ ( sym(*-identityʳ x))) ⟩
((x * 0#) + (x * 1#)) - x ≈⟨ +-congʳ (sym(distribˡ _ _ _ )) ⟩
(x * (0# + 1#)) - x ≈⟨ +-congʳ (*-congˡ ( +-identityˡ 1# )) ⟩
(x * (1#)) - x ≈⟨ +-congʳ (*-identityʳ x) ⟩
x - x ≈⟨ -‿inverseʳ x ⟩
0# ∎
Similarly, we can prove left zero. This proof should be used in -‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y and -‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y
Also in the literature, I don't see zero given in the definition. Was this part of some design decision?