proposition: Lemma isdecisbndqdec ( P : nat -> hProp ) ( is : isdecnatprop P ) ( n : nat ) : ( forall m : nat, natleh m n -> P m ) ⨿ ∃ m : nat, natleh m n × neg ( P m ).
proof: Proof. destruct ( bndexistsisdecnatprop _ ( negisdecnatprop P is ) n ) as [ l | r ]. - apply ii2. assumption. - apply ii1. intros m j. destruct ( is m ) as [ l' | r' ]. + assumption. + apply fromempty. apply r. apply total2tohexists. split with m. split; assumption. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids