proposition: Lemma onth_tnth {n} (s : n.-tuple A) (i : 'I_n) : onth s i = Some (tnth s i).
proof: Proof. elim: n s i =>[|n IH] s i; first by case: i. case/tupleP: s=>/=x s; case: (unliftP ord0 i)=>[j|]-> /=. - by rewrite tnthS. by rewrite tnth0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)