proposition: Lemma expr_conv_mono n n1 n2 q r : 0 < q :> R -> q <= r -> (n1 <= n2 <= n)%nat -> r ^+ (n - n2) * q ^+ n2 <= r ^+ (n - n1) * q ^+ n1.
proof: Proof. move=> /[dup] /ltW q0 q1 qr /andP [] n12 n2n. have r1 := lt_le_trans q1 qr. have r0 := ltW r1. rewrite [leLHS](_ : _ = q ^+ n1 * q ^+ (n2 - n1)%nat * r ^+ (n - n2)%nat); last by rewrite -exprD subnKC // mulrC. rewrite [leRHS](_ : _ = q ^+ n1 * r ^+ (n2 - n1)%nat * r ^+ (n - n2)%nat); last by rewrite -mulrA -exprD addnBAC // subnKC // mulrC. apply: ler_pM => //; [by apply/mulr_ge0; apply/exprn_ge0 | by apply/exprn_ge0 | ]. apply: ler_pM => //; [by apply/exprn_ge0 | by apply/exprn_ge0 |]. rewrite -[leLHS]mul1r -ler_pdivlMr ?exprn_gt0 // -expr_div_n. apply: exprn_ege1. by rewrite ler_pdivlMr // mul1r. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum zmodp matrix lra) mathcomp(mathcomp_extra classical_sets Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist entropy binary_entropy_function channel hamming channel_code pproba