Lemma dni_last {n : nat} (i: ⟦n⟧ ) : pr1 (dni lastelement i) = i. Proof. intros. induction i as [i I]. unfold dni,di. simpl. induction (natlthorgeh i n) as [g|g]. { apply idpath. } simpl. contradicts (natlehtonegnatgth _ _ g) I. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.