proposition: Lemma Xpos a : 0 < X a.
proof: Proof. move/nesym/INR_not_0 : (@Xnon0 a) => H. by rewrite ltR0n ltn_neqAle /= leq0n andbT; apply/eqP/nesym. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code