proposition: Lemma negisdecnatprop ( P : nat -> hProp ) ( is : isdecnatprop P ) : isdecnatprop ( fun n : nat => hneg ( P n ) ).
proof: Proof. intros n. destruct ( is n ) as [ l | r ]. - apply ii2. intro j. assert hfalse as x. { simpl in j. apply j. assumption. } apply x. - apply ii1. 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