proposition: Lemma onth_sizeP s n : onth_spec s n (n < size s).
proof: Proof. elim: s n=>/= [|a s IH] n; first by rewrite ltn0; constructor. case: n=>[|n] /=; first by apply: (@onth_some _ _ a). rewrite ltnS; case: (IH n)=>[|v] H. - by constructor. by apply: (@onth_some _ _ v). Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)