proposition: Lemma Pr_lt1 E : Pr E < 1 <-> Pr E != 1.
proof: Proof. split => H; move: (Pr_1 E); rewrite leR_eqVlt. by move=> [Pr1|]; [move: H; rewrite Pr1 => /ltRR|exact: ltR_eqF]. by move=> [Pr1|//]; rewrite Pr1 eqxx in H. 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