proposition: Corollary isdeceqstn ( n : nat ) : isdeceq (⟦n⟧).
proof: Proof. unfold isdeceq. intros x x'. apply (isisolatedinstn x x' ). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions