proposition: Lemma dni_last {n : nat} (i: ⟦n⟧ ) : pr1 (dni lastelement i) = i.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions