proposition: Lemma prefix_onth s t 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 _)). by case/prefix_cons': H2=><- H2; case: x H1=>[|n] //= H1; apply: IH. 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)