proposition: Corollary lastelement_eq : ∏ (n : nat) (i : ⟦S n⟧ ) (e : pr1 i = n), i = lastelement.
proof: Proof. intros n i e. unfold lastelement. apply isinjstntonat. apply e. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions