Lemma isapropnatdecleast ( F : nat -> UU ) ( is : ∏ n , isdecprop ( F n ) ) : isaprop ( natdecleast F is ). Proof. intros. set ( P := λ n' : nat, make_hProp _ ( is n' ) ). assert ( int1 : ∏ n : nat, isaprop ( ( F n ) × ( ∏ n' : nat , F n' -> natleh n n' ) ) ). { intro n. apply isapropdirprod. - apply ( pr2 ( P n ) ). - apply impred. intro t. apply impred. intro. apply ( pr2 ( natleh n t ) ). } set ( int2 := ( λ n : nat, make_hProp _ ( int1 n ) ) : nat -> hProp ). change ( isaprop ( total2 int2 ) ). apply isapropsubtype. intros x1 x2. intros c1 c2. simpl in *. destruct c1 as [ e1 c1 ]. destruct c2 as [ e2 c2 ]. set ( l1 := c1 x2 e2 ). set ( l2 := c2 x1 e1 ). apply ( isantisymmnatleh _ _ l1 l2 ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.