proposition: Lemma prefix_same_size a b : prefix a b -> size a = size b -> a = b.
proof: Proof. case/prefixP => c /eqP/esym ->{b} /eqP. rewrite size_cat -{1}(addn0 (size a)) eqn_add2l eq_sym size_eq0 => /eqP ->. by rewrite cats0. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext