proposition: Lemma nnpp_prefix (C : code_set T) : (~ prefix_code C -> False) -> prefix_code C.
proof: Proof. move=> H c c' cC c'C cc'. apply/negP => prefix_cc'; apply H => abs. move: (abs _ _ cC c'C cc'); by rewrite prefix_cc'. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext