Lemma isdeceqtoisapartdec ( X : hSet ) ( is : isdeceq X ) : isapartdec ( tpair _ ( deceqtoneqapart is ) ). Proof. intros a b. destruct ( is a b ) as [ l | r ]. - apply ii2. assumption. - apply ii1. intros f. apply r. assumption. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.