proposition: Lemma dni_last_lt {n : nat} (j : ⟦ n ⟧) : dni lastelement j < @lastelement n.
proof: Proof. intros. induction j as [j J]. simpl. unfold di. induction (natlthorgeh j n) as [L|M]. - exact J. - apply fromempty. exact (natlthtonegnatgeh _ _ J M). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions