proposition: Lemma isdecbexists ( n : nat ) ( P : nat -> UU ) ( is : ∏ n' , isdecprop ( P n' ) ) : isdecprop ( hexists ( λ n', ( natleh n' n ) × ( P n' ) ) ).
proof: Proof. intros. set ( P' := λ n' : nat, make_hProp _ ( is n' ) ). induction n as [ | n IHn ]. - apply ( isdecpropweqb ( weqexistsnatlehn0 P' ) ). apply ( is 0 ). - apply ( isdecpropweqb ( weqexistsnatlehnsn' _ P' ) ). apply isdecprophdisj. + apply IHn. + apply ( is ( S n ) ). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions