Lemma isdecbforall ( n : nat ) ( P : nat -> UU ) ( is : ∏ n' , isdecprop ( P n' ) ) : isdecprop ( ∏ n' , natleh n' n -> P n' ). Proof. intros. set ( P' := λ n' : nat, make_hProp _ ( is n' ) ). induction n as [ | n IHn ]. - apply ( isdecpropweqb ( weqforallnatlehn0 P' ) ). apply ( is 0 ). - apply ( isdecpropweqb ( weqforallnatlehnsn' _ P' ) ). apply isdecpropdirprod. + apply IHn. + apply ( is ( S n ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.