Lemma deceqtoneqapart { X : UU } ( is : isdeceq X ) : isapart ( neq X ). Proof. intros. split. - intros a p. simpl in p. apply p. apply idpath. - split. + intros a b p q. simpl in p. apply p. apply pathsinv0. assumption. + intros a c b p P s. apply s. destruct ( is a c ) as [ l | r ]. * apply ii2. rewrite <- l. assumption. * apply ii1. 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.