proposition: Lemma f0 : forall x, (0 <= f x)%mcR.
proof: Proof. move=> x; rewrite ffunE; apply/RleP; move: x. rewrite (_ : 0%mcR = 0)//. case => -[ [? [[|[|[|[|[]//]]]]] | [? [[|[|[|[|[]//]]]]] | [? [[|[|[|[|[]//]]]]] | [? [[|[|[|[|[]//]]]]] | []//]]]]]; rewrite /f /=; try lra. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup finalg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond entropy