Definition fpsapart ( R : acommring ) : apart ( fpscommring R ). Proof. intros. split with ( fpsapart0 R ). split. - intros s f. assert ( hfalse ) as i. { use (hinhuniv _ f). intro k. destruct k as [ n p ]. apply (acommring_airrefl R ( s n ) p). } apply i. - split. + intros s t p P j. use (hinhuniv _ p). intro k. destruct k as [ n q ]. apply j. split with n. apply ( acommring_asymm R ( s n ) ( t n ) q ). + intros s t u p P j. use (hinhuniv _ p). intro k. destruct k as [ n q ]. use ( hinhuniv _ (acommring_acotrans R ( s n ) ( t n ) ( u n ) q ) ). intro l. destruct l as [ l | r ]. * apply j. apply ii1. intros v V. apply V. split with n. assumption. * apply j. apply ii2. intros v V. apply V. split with n. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.