proposition: Lemma w_ub (H : kraft_cond R T l) j : w j <= #|T|^(nth O l j) - 1.
proof: Proof. have H' : (\sum_(i < n) #|T|%:R^-(nth O l i) <= (1 : R))%R. move: H; by rewrite /kraft_cond (_ : size l = n). rewrite -(@ler_nat R) -(@ler_pM2l _ (#|T|%:R ^- nth O l j))%R; last first. by rewrite -exprVn exprn_gt0 // invr_gt0 ltr0n card_ord. case/boolP : (j == ord0) => [/eqP ->|i0]. by rewrite wE0 mulr0 mulr_ge0 // -exprVn exprn_ge0 // invr_ge0 ler0n. rewrite !natrB ?expn_gt0 ?card_ord // -!natrX. rewrite mulrBr mulVr ?unitfE ?mulr1 ?pnatr_eq0 ?expn_eq0 //. rewrite /w // natr_sum big_distrr /=. rewrite (eq_bigr (fun j : 'I__ => #|T|%:R ^-nth O l j))%R; last first. move=> i _; rewrite !natrX card_ord 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. by rewrite mulrA mulVr ?unitfE -?natrX ?pnatr_eq0 ?expn_eq0 // mul1r. rewrite lerBrDr natrX (le_trans _ H') //. rewrite [X in (X <= _)%R](_ : _ = \sum_(k < j.+1) #|T|%:R^-nth O l k)%R; last first. by rewrite big_ord_recr /= card_ord. rewrite (@big_ord_widen _ _ _ j.+1 n (fun i => #|T|%:R ^- nth O l i))%R //. rewrite [in X in (_ <= X)%R](bigID (fun k : 'I_n => k < j.+1)) /= lerDl. rewrite sumr_ge0 // => k _; by rewrite invr_ge0 exprn_ge0 // ler0n. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext