Lemma iscommfpsplus ( R : commring ) : iscomm ( fpsplus R ). 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.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.