proposition: Lemma f1 (a : A) : \sum_(a' : {:option A}) f a a' = 1.
proof: Proof. rewrite (bigD1 None) //= (bigD1 (Some a)) //= !ffunE eqxx /=. rewrite [X in _ + (_ + X)](_ : _ = 0). by rewrite GRing.addr0 onemKC. apply/eqP; rewrite psumr_eq0/=; last first. - rewrite /f; case => [a'|]; last by case: p_01. rewrite ffunE. case: ifPn => [_ _|//]. by case: p_01 => ? ?; apply/onem_ge0/RleP. - apply/allP; case => //= a' aa'; rewrite ffunE; case: ifPn => // /eqP ?. subst a'. by move: aa'; rewrite eqxx. by rewrite eqxx implybT. Qed.
imports: mathcomp(all_ssreflect all_algebra matrix) Reals mathcomp(mathcomp_extra Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy binary_entropy_function channel hamming channel_code