proposition: Lemma bin_ent_0eq0 : H2 0 = 0.
proof: Proof. rewrite /H2 /log. by rewrite !(Log_1, mulR0, mul0R, oppR0, mul1R, mulR1, add0R, addR0, subR0). Qed.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb