proposition: Lemma mpos eps : 0 <> INR n -> 0 < (m eps)%:R.
proof: Proof. rewrite /m => nnon0. rewrite (_ : 0 = INR 0)//; apply: lt_INR. rewrite {1}(_ : 0%nat = Z.abs_nat 0)//; apply: Zabs_nat_lt; split => //. apply: lt_0_IZR. apply: (@ltR_trans (exp (m' eps) - 1)); last exact: (proj1 (floorP _)). rewrite -(@ltR_add2r 1) addRC /Rdiv -addRA Rplus_opp_l 2!addR0 -{1}exp_0. apply: exp_increasing. rewrite (_ : 0 = INR 0) //; apply: lt_INR; apply: ltP. apply: (@leq_trans (m'' eps)); last exact: leq_maxr. by apply: (@leq_trans 1); last exact: leq_maxr. 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