Definition negstn0 : ¬ (⟦0⟧). Proof. intro x. destruct x as [ a b ]. apply ( negnatlthn0 _ b ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.