proposition: Lemma Ind_inP (s : {set A}) (x : A) : reflect (Ind s x = R1) (x \in s).
proof: Proof. apply: (iffP idP); rewrite /Ind; first by move->. by case: ifP =>//; auto with real. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist