proposition: Lemma size_onth s n : n < size s -> exists x, onth s n = Some x.
proof: Proof. by case: onth_sizeP=>// v H _; exists 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)