proposition: Lemma quotientringsumdecom ( X : commring ) ( R : ringeqrel ( X := X ) ) ( a b : X ) : @op2 ( commringquot R ) ( setquotpr R a ) ( setquotpr R b ) = ( setquotpr R ( a * b )%ring ).
proof: Proof. intros. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble