Lemma negbforalldectototal2neg ( n : nat ) ( P : nat -> UU ) ( is : ∏ n' : nat , isdecprop ( P n' ) ) : ¬ ( ∏ n' : nat , natleh n' n -> P n' ) -> total2 ( λ n', ( natleh n' n ) × ¬ ( P n' ) ). Proof. set ( P' := λ n' : nat, make_hProp _ ( is n' ) ). induction n as [ | n IHn ]. - intro nf. set ( nf0 := negf ( invweq ( weqforallnatlehn0 P' ) ) nf ). split with 0. apply ( make_dirprod ( isreflnatleh 0 ) nf0 ). - intro nf. set ( nf2 := negf ( invweq ( weqforallnatlehnsn' n P' ) ) nf ). set ( nf3 := fromneganddecy ( is ( S n ) ) nf2 ). destruct nf3 as [ f1 | f2 ]. + set ( int := IHn f1 ). destruct int as [ n' d2 ]. destruct d2 as [ l np ]. split with n'. split with ( natlehtolehs _ _ l ). apply np. + split with ( S n ). split with ( isreflnatleh _ ). apply f2. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.