proposition: Lemma bsc_prob_prop (p : {prob R}) n : Prob.p p < 1 / 2 -> forall n1 n2 : nat, (n1 <= n2 <= n)%nat -> ((1 - Prob.p p) ^ (n - n2) * (Prob.p p) ^ n2 <= (1 - Prob.p p) ^ (n - n1) * (Prob.p p) ^ n1)%R.
proof: Proof. move=> p05 d1 d2 d1d2. case/boolP: (p == 0%:pr). move/eqP->; rewrite !coqRE; apply/RleP. rewrite probpK subr0 !expr1n !mul1r !expr0n. move: d1d2; case: d2; first by rewrite leqn0 => /andP [] ->. case: (d1 == 0%nat) => //=. move=> ? ?; exact:ler01. move/prob_gt0 => p1. rewrite !coqRE. apply/RleP/expr_conv_mono => //. lra. 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