Lemma fpsapartisbinopapartplusl ( R : acommring ) : isbinopapartl ( fpsapart R ) ( @op1 ( fpscommring R ) ). Proof. intros. intros a b c p. intros P s. use (hinhuniv _ p). intro k. destruct k as [ n q ]. apply s. change ( ( a + b ) n ) with ( ( a n ) + ( b n ) ) in q. change ( ( a + c ) n ) with ( ( a n ) + ( c n ) ) in q. split with n. apply ( pr1 ( acommring_aadd R ) ( a n ) ( b n ) ( c n ) q ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.