proposition: Lemma iscommfpsplus ( R : commring ) : iscomm ( fpsplus R ).
proof: Proof. intros. unfold iscomm. intros s t. unfold fpsplus. change ((fun n : nat => s n + t n) = (fun n : nat => t n + s n) ). apply funextfun. intro n. set (H1:= pr2 (pr1 (pr1 (pr1 (pr2 R))))). apply H1. Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers