proposition: Lemma prefix_trans s2 s1 s3 : prefix s1 s2 -> prefix s2 s3 -> prefix s1 s3.
proof: Proof. by move=>H1 H2 n x E; apply: H2; apply: H1. 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)