Lemma commringquotprandop1 { A : commring } ( R : @ringeqrel A ) ( a b : A ) : @op1 ( commringquot R ) ( setquotpr ( pr1 R ) a ) ( setquotpr ( pr1 R ) b ) = setquotpr ( pr1 R ) ( a + b ). Proof. intros. change ( @op1 ( commringquot R ) ) with ( setquotfun2 R R ( @op1 A ) ( pr1 ( iscomp2binoptransrel ( pr1 R ) ( eqreltrans _ ) ( pr2 R ) ) ) ). unfold setquotfun2. rewrite setquotuniv2comm. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.