Theorem accth ( F : nat -> UU ) ( is : ∏ n , isdecprop ( F n ) ) ( is' : hexists F ) : natdecleast F is. Proof. revert is'. simpl. apply (@hinhuniv _ ( make_hProp _ ( isapropnatdecleast F is ) ) ). intro t2. destruct t2 as [ n l ]. simpl. set ( F' := λ n' : nat, hexists ( λ n'', ( natleh n'' n' ) × ( F n'' ) ) ). assert ( X : ∏ n' , F' n' -> natdecleast F is ). { intro n'. induction n' as [ | n' IHn' ]. - apply ( @hinhuniv _ ( make_hProp _ ( isapropnatdecleast F is ) ) ). intro t2. destruct t2 as [ n'' is'' ]. destruct is'' as [ l'' d'' ]. split with 0. split. + set ( e := natleh0tois0 l'' ). clearbody e. destruct e. apply d''. + apply ( λ n', λ f : _, natleh0n n' ). - apply ( @hinhuniv _ ( make_hProp _ ( isapropnatdecleast F is ) ) ). intro t2. destruct t2 as [ n'' is'' ]. set ( j := natlehchoice2 _ _ ( pr1 is'' ) ). destruct j as [ jl | je ]. + simpl. apply ( IHn' ( hinhpr ( tpair _ n'' ( make_dirprod jl ( pr2 is'' ) ) ) ) ). + simpl. rewrite je in is''. destruct is'' as [ nn is'' ]. clear nn. clear je. clear n''. assert ( is' : isdecprop ( F' n' ) ) by apply ( isdecbexists n' F is ). destruct ( pr1 is' ) as [ f | nf ]. * apply ( IHn' f ). * split with ( S n' ). split with is''. intros n0 fn0. destruct ( natlthorgeh n0 ( S n' ) ) as [ l' | g' ]. -- set ( i' := natlthtolehsn _ _ l' ). destruct ( nf ( hinhpr ( tpair _ n0 ( make_dirprod i' fn0 ) ) ) ). -- apply g'. } apply ( X n ( hinhpr ( tpair _ n ( make_dirprod ( isreflnatleh n ) l ) ) ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.