finish proof of is_lim_seq_ps_p_event_ge_event_lt

Signed-off-by: Avi Shinnar <[email protected]>
IBM · Dec 21, 2023 · 7ab3d71 · 7ab3d71
1 parent bb0c700
commit 7ab3d71
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/coq/ProbTheory/RandomVariableL2.v b/coq/ProbTheory/RandomVariableL2.v
@@ -523,15 +523,15 @@ Section L2.
    {
      intros.
      rewrite <- ps_complement.
-     f_equal.
-     admit.
+     apply ps_proper.
+     split; simpl; unfold pre_event_complement; lra.
    }
    apply (is_lim_seq_ext _ _ 1 H0).
    apply is_lim_seq_minus with (l1 := 1) (l2 := 0); trivial.
    - apply is_lim_seq_const.
    - unfold is_Rbar_minus, is_Rbar_plus.
      simpl; f_equal; f_equal; lra.
-  Admitted.     
+ Qed.
 
 
  Lemma conv_l1_prob_alt