Lemma negisdecnatprop ( P : nat -> hProp ) ( is : isdecnatprop P ) : isdecnatprop ( fun n : nat => hneg ( P n ) ). Proof. intros n. destruct ( is n ) as [ l | r ]. - apply ii2. intro j. assert hfalse as x. { simpl in j. apply j. assumption. } apply x. - 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.