Lemma dni_last_lt {n : nat} (j : ⟦ n ⟧) : dni lastelement j < @lastelement n. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.