proposition: Lemma decode_morphism_and_ops `{InVariety theory x} `{InVariety theory y} `{!HomoMorphism theory x y f}: SemiRing_Morphism (f tt).
proof: Proof. pose proof (preserves theory x y f) as P. repeat (constructor; try apply _) ; [ apply (P plus) | apply (P zero) | apply (P mult) | apply (P one) ]. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics