proposition: Lemma open_interval_convex a b (Hab : (a < b)%coqR) : is_convex_set (fun x => a < x < b)%coqR.
proof: Proof. apply/asboolP => x y t [xa xb] [ya yb]. have [->|t0] := eqVneq t 0%:pr; first by rewrite conv0. have [->|t1] := eqVneq t 1%:pr; first by rewrite conv1. apply conj. - rewrite -[X in (X < Prob.p t * x + (Prob.p t).~ * y)%coqR]mul1r -(onemKC (Prob.p t)). rewrite (mulrDl _ _ a) -RplusE. apply ltR_add; rewrite ltR_pmul2l //; [exact/RltP/prob_gt0 | exact/RltP/onem_gt0/prob_lt1]. - rewrite -[X in (_ + _ < X)%coqR]mul1r. rewrite -(onemKC (Prob.p t)). rewrite mulrDl. apply ltR_add; rewrite ltR_pmul2l //; [exact/RltP/prob_gt0 | exact/RltP/onem_gt0/prob_lt1]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist