proposition: Corollary dni_lastelement_eq : ∏ (n : nat) (i : ⟦S n⟧ ) (ie : pr1 i < n), i = dni_lastelement (make_stn n (pr1 i) ie).
proof: Proof. intros n i ie. apply isinjstntonat. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions