proposition: Lemma onem_half: onem 2^-1 = 2^-1.
proof: Proof. have ne20: (2 : R_ringType) != 0 by rewrite intr_eq0. apply (mulfI ne20). by rewrite mulrBr mulr1 divff// -pmulrn mulr2n -addrA subrr addr0. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals