proposition: Lemma Ind_notinP (s : {set A}) (x : A) : reflect (Ind s x = R0) (x \notin s).
proof: Proof. apply: (iffP idP); rewrite /Ind => Hmain. by rewrite ifF //; exact: negbTE. by apply: negbT; case: ifP Hmain =>// _ H10; exfalso; 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