proposition: Lemma prefix_implies_kraft_cond : prefix_code C -> 0 < #|T| -> kraft_cond R T (map size C).
proof: Proof. move=> prefixC T_gt0; rewrite /kraft_cond size_map -/n. have /ler_pM2l <- : ((0 : R) < #|T|%:R ^+ lmax)%R. by rewrite exprn_gt0 // ltr0n. rewrite mulr1 big_distrr /=. rewrite (eq_bigr (fun i : 'I_n => #|suffixes C``_i|%:R)%R); last first. move=> i _; rewrite card_suffixes; last by apply/nthP; exists i. rewrite natrX exprB // ?(nth_map [::]) //. by apply/leq_lmax/nthP; exists i. by rewrite unitfE pnatr_eq0 -lt0n. apply (@le_trans _ _ (#|\bigcup_(i < n) suffixes (C ``_ i)|%:R)%R). rewrite -sum1_card. rewrite partition_disjoint_bigcup /=. rewrite natr_sum ler_sum // => i _. by rewrite sum1_card. move=> i j ij. rewrite -setI_eq0 disjoint_suffixes //. by apply/nthP; exists i. by apply/nthP; exists j. by rewrite nth_uniq //; case: C. by rewrite -natrX -card_tuple ler_nat max_card. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext