proposition: Lemma fdistI2E a : fdistI2 a = if a == ord0 then p : R else (Prob.p p).~.
proof: Proof. rewrite /fdistI2 fdist_binaryE; case: ifPn => [/eqP ->|]. by rewrite eq_sym (negbTE (neq_lift _ _)). by case: ifPn => //; move: a => -[[//|[|]//]]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext