proposition: Lemma onth_nth x0 n s : n < size s -> onth s n = Some (nth x0 s n).
proof: Proof. elim: s n=>//= a s IH n. by rewrite ltnS; case: n. 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)