Lemma isdecisbndqdec ( P : nat -> hProp ) ( is : isdecnatprop P ) ( n : nat ) : ( forall m : nat, natleh m n -> P m ) ⨿ ∃ m : nat, natleh m n × neg ( P m ). Proof. destruct ( bndexistsisdecnatprop _ ( negisdecnatprop P is ) n ) as [ l | r ]. - apply ii2. assumption. - apply ii1. intros m j. destruct ( is m ) as [ l' | r' ]. + assumption. + apply fromempty. apply r. apply total2tohexists. split with m. split; 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.