proposition: Lemma size_onth (s : seq A) n : n < size s -> exists x, onth s n = Some x.
proof: Proof. elim:s n=>[//|x' s' IH] [|n] /=. - by move=>_; exists x'. rewrite -(addn1 n) -(addn1 (size s')) ltn_add2r. by apply: IH. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq)