proposition: Lemma prefix_codeP C : prefix_code C <-> prefix_code_strong C.
proof: Proof. split. move=> H c c' cC c'C cc' _. by apply H. move=> H c c' cC c'C cc'. case/boolP : (size c <= size c') => [K|]; first exact: H. apply: contra => /eqP K. by rewrite -(cat_take_drop (size c) c') {1}K size_cat leq_addr. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext