proposition: Lemma dni_lastelement_ord {n : nat} : ∏ i j: ⟦n⟧, i≤j -> dni_lastelement i ≤ dni_lastelement j.
proof: Proof. intros ? ? e. exact e. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions