proposition: Lemma prefix_onth (s t : seq A) x : x < size s -> prefix s t -> onth s x = onth t x.
proof: Proof. elim:s t x =>[//|a s IH] [|b t] x H1 H2; first by move: (H2 0 a (erefl _)). apply prefix_cons' in H2. case: x H1=>[_|n H1]; first by rewrite (proj1 H2). by apply: IH=>//; exact (proj2 H2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq)