nth_seq_rev@{} {n i} (H : (i < n)%nat) : nth (seq_rev n) i = Some (n - i.+1)%nat. Proof. induction i as [|i IHi] in n, H |- *. - induction n. 1: destruct (not_lt_zero_r _ H). cbn; by rewrite nat_sub_zero_r. - induction n as [|n IHn]. 1: destruct (not_lt_zero_r _ H). by apply IHi, leq_pred'. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum