Lemma bndexistsisdecnatprop ( P : nat -> hProp ) ( is : isdecnatprop P ) : isdecnatprop ( fun n : nat => ∃ m : nat, natleh m n × P m ). Proof. intros n. induction n. - destruct ( is 0%nat ) as [ l | r ]. + apply ii1. apply total2tohexists. split with 0%nat. split. * apply isreflnatleh. * assumption. + apply ii2. intro j. assert hfalse as x. { simpl in j. apply j. intro m. destruct m as [ m m' ]. apply r. change ( natleh m 0 × P m ) in m'. rewrite ( natleh0tois0 ( pr1 m' ) ) in m'. apply (pr2 m'). } apply x. - destruct ( is ( S n ) ) as [ l | r ]. + apply ii1. apply total2tohexists. split with ( S n ). split. * apply ( isreflnatleh ( S n ) ). * assumption. + destruct IHn as [ l' | r' ]. * apply ii1. use (hinhuniv _ l'). intro m. destruct m as [ m m' ]. apply total2tohexists. split with m. split. -- apply ( istransnatleh(m := n) ). ++ apply m'. ++ apply natlthtoleh. apply natlthnsn. -- apply (pr2 m'). * apply ii2. intro j. apply r'. use (hinhuniv _ j). intro m. destruct m as [ m m' ]. -- apply total2tohexists. split with m. split. ++ destruct ( natlehchoice m ( S n ) ( pr1 m' ) ) as [ h | p ]. ** apply natlthsntoleh. assumption. ** apply fromempty. apply r. rewrite <- p. apply (pr2 m'). ++ apply (pr2 m'). 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.