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. intros. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.