proposition: Lemma Rxx2 x : x = x * x -> x = 0 \/ x = 1.
proof: Proof. case/boolP: (x == 0) => Hx. rewrite (eqP Hx); by left. move/(f_equal (Rdiv ^~ x)). rewrite divRR // /Rdiv -mulRA mulRV // mulR1 => <-; by right. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba