Definition compute_pr1_dni_last (n : nat) (i: ⟦n⟧ ) : pr1 (dni lastelement i) = pr1 i. Proof. intros. unfold dni,di; simpl. induction (natlthorgeh i n) as [q|q]. - apply idpath. - contradicts (pr2 i) (natlehneggth q). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.