proposition: Lemma preserves_0: f 0 = 0.
proof: Proof. Proof (preserves_mon_unit (f:=f)). Lemma preserves_1: f 1 = 1. Proof (preserves_mon_unit (f:=f)). Lemma preserves_mult: ∀ x y, f (x * y) = f x * f y. Proof. intros. apply preserves_sg_op. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra