Theorem apartdectoisaintdomfps ( R : aintdom ) ( is : isacommringapartdec R ) : aintdom. Proof. revert is. split with ( acommringfps R ). split. - intros P s. apply s. split with 0%nat. change ( @ringunel1 ( fpscommring R ) 0%nat ) with ( @ringunel1 R ). change ( @ringunel2 R # ( @ringunel1 R ) ). apply R. - intros a b p q. use (hinhuniv _ p). intro n. destruct n as [ n n0 ]. apply ( apartdecintdom0 R is n); assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.