nth_seq@{} {n i} (H : (i < n)%nat) : nth (seq n) i = Some i. Proof. induction n. 1: destruct (not_lt_zero_r _ H). rewrite seq_succ. destruct (dec (i < n)%nat) as [H'|H']. - lhs nrapply nth_app. 1: by rewrite length_seq. by apply IHn. - apply geq_iff_not_lt in H'. apply leq_pred' in H. destruct (leq_antisym H H'). lhs nrapply nth_last. { rewrite length_app. rewrite nat_add_comm. apply length_seq. } nrapply last_app. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum