proposition: Lemma prefix_rcons x s : prefix s (rcons s x).
proof: Proof. by elim: s=>//= y ys IH; apply/prefix_cons; 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)