proposition: Lemma deceqtoneqapart { X : UU } ( is : isdeceq X ) : isapart ( neq X ).
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids