proposition: Lemma kraft_implies_prefix : kraft_cond R T l -> exists C : code_set T, prefix_code C.
proof: Proof. move=> H; exists (ACode _ l_n sorted_l). apply nnpp_prefix. move=> /(if_not_prefix l_neq0 H) /existsP[j /existsP[ k /andP[jk pre]]]. pose r := ((w k)%:R / #|T|%:R^+(l``_k - l``_j) : R)%R. have H1 : (r >= (w j)%:R + (1 : R))%R. pose r' := (\sum_(i < k) #|T|%:R ^+ l``_j * #|T|%:R ^- l``_i : R)%R. have -> : r = r'. rewrite /r /r' natr_sum big_distrl /=; apply/eq_bigr => i _. have ? : (#|T|%:R ^+ (l ``_ k - l ``_ j) : R)%R \is a GRing.unit. by rewrite unitfE expf_eq0 card_ord pnatr_eq0 andbF. apply: (@mulIr _ (#|T|%:R ^+ (l``_k - l``_j))%R) => //. rewrite natrX -mulrA mulVr // mulr1 exprB; last 2 first. apply/(sorted_ltn_nth leq_trans) => //; rewrite inE l_n //. by rewrite (leq_trans (ltn_ord i)) // ltnW. by rewrite unitfE pnatr_eq0 card_ord. rewrite exprB; last 2 first. by apply/(sorted_ltn_nth leq_trans) => //; rewrite inE l_n. by rewrite unitfE pnatr_eq0 card_ord. rewrite mulrCA mulrAC mulrV // ?mul1r //. by rewrite unitfE -natrX pnatr_eq0 expn_eq0 card_ord. pose u := (\sum_(j<=i<k) #|T|%:R ^+ l``_j * #|T|%:R ^- l``_i : R)%R. have -> : (r' = (w j)%:R + u :> R)%R. pose f := (fun i : nat => #|T|%:R^+l``_j * #|T|%:R^-l``_i : R)%R. case/boolP : (j == ord0) => j0. rewrite /u (eqP j0) wE0 add0r big_mkord /r'. apply/eq_bigr => i _; by rewrite (eqP j0). rewrite /r' /u -(big_mkord xpredT f)%R natr_sum. rewrite (eq_bigr (fun i : 'I__ => f i)); last first. move=> i _; rewrite natrX exprB //. apply/(sorted_ltn_nth leq_trans) => //; rewrite inE l_n //. by rewrite (leq_trans (ltn_ord i)) // ltnW. by rewrite unitfE pnatr_eq0 card_ord. by rewrite -(big_mkord xpredT f)%R -big_cat_nat //= ltnW. rewrite lerD //. rewrite /u -(@prednK k); last by rewrite (leq_ltn_trans _ jk). rewrite big_nat_recl; last by move/(leq_sub2r 1) : jk; rewrite !subn1. rewrite divrr ?unitfE -?natrX ?pnatr_eq0 ?expn_eq0 ?card_ord //. rewrite lerDl sumr_ge0 // => i _. by rewrite natrX divr_ge0 // exprn_ge0 // ?card_ord ?ler0n. have H2 : (r - 1 < (w j)%:R)%R. have /(congr1 (fun x => x%:R : R)%R) : w k = w j * #|T| ^ (l``_k - l``_j) + w k %% #|T| ^ (l``_k - l``_j). have := prefix_modn pre. do 2 rewrite nat_of_ary_cat nat_of_ary_nseq0 mul0n add0n ary_of_natK. by rewrite !size_cat !size_nseq !subnK // size_ary_of_nat // -/t -(card_ord t) (w_sub l_n sorted_l H). rewrite natrD => /(congr1 (fun x => x / #|T|%:R^+(l``_k - l``_j)))%R. rewrite -/r mulrDl natrM natrX mulrK; last first. by rewrite unitfE expf_eq0 card_ord pnatr_eq0 andbF. move=> wkE. have : ((w k %% #|T| ^ (l``_k - l``_j))%:R / #|T|%:R ^+ (l``_k - l``_j) < (1 : R))%R. rewrite ltr_pdivrMr; [|by rewrite -natrX ltr0n expn_gt0 card_ord]. by rewrite mul1r -natrX ltr_nat ltn_mod expn_gt0 card_ord. by rewrite {}wkE ltrBDl addrC ltrD2r. by rewrite ltrBlDl addrC ltNge H1 in H2. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext