proposition: Lemma han : n.-1%:R * `H P <= \sum_(i < n) `H (fdist_col' P i).
proof: Proof. rewrite -subn1 natrB // -RmultE mulRBl mul1R. apply/RleP; rewrite leR_subl_addr {2}(chain_rule_rV P). rewrite -big_split /= -{1}(card_ord n) -sum1_card. rewrite -INRE big_morph_natRD big_distrl /=. apply leR_sumR => i _; rewrite mul1R. case: ifPn => [/eqP|] i0. rewrite (_ : i = ord0); last exact/val_inj. rewrite -tail_of_fdist_rV_fdist_col' /tail_of_fdist_rV /head_of_fdist_rV. rewrite -{1}(fdist_rV_of_prodK P) entropy_fdist_rV_of_prod. move: (chain_rule (fdist_prod_of_rV P)); rewrite /joint_entropy => ->. by rewrite [in X in (_ <= X)%R]addRC leR_add2l -fdistX1; exact: information_cant_hurt. rewrite (chain_rule_multivar _ i0) leR_add2l. by apply/RleP; exact/han_helper. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence