Ssreflect probabilities (event and not event) sum to one

Question

I am a beginner and would like your help getting to sum the probability of event F and the probability of event not F to one. Is there a fast way forward?

X: {RV (P) -> (R)}
F: {set U}
H: 0 < Pr P F
H0: Pr P F < 1
i: U
H1: i \in U

===

X i * P i * ((if i \in F then R1 else R0) + (if i \in ~: F then R1 else R0)) =
X i * P i

Answer 1

Looks to me like you need to rewrite with inE so that i \in ~: F become i \notin F and then a case analysis (case: (i \in F)) followed by rewrite (addr0, add0r) mulr1 might suffice.