proposition: Lemma prefix_cons x y a b : prefix (x :: a) (y :: b) = (x == y) && prefix a b.
proof: Proof. rewrite /prefix /=; by apply/eqP/andP => [[-> {1}-> //]|[/eqP -> /eqP <-]]. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext