proposition: Lemma probinvn1 : probinvn 1 = 2^-1 :> R_numFieldType.
proof: Proof. rewrite /R_numFieldType /GRing.inv /= /Rinvx. case:ifP=>// /negbFE. by rewrite/Rdefinitions.IZR intr_eq0. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals