proposition: Theorem Bernoulli_correct : forall (r : Rat), r <= 1 -> Pr[Bernoulli r] == r.
proof: Proof. unfold Bernoulli. intuition. destruct r. rewrite RndNat_seq. rewrite (sumList_filter_partition (fun z => if (lt_dec z n) then true else false)). eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply ratAdd_eqRat_compat. eapply sumList_all. intros. destruct ( lt_dec a n). simpl. destruct ( EqDec_dec bool_EqDec true true). eapply eqRat_refl. intuition. apply filter_In in H0. intuition. exfalso. destruct (lt_dec a n); intuition. eapply sumList_0. intros. apply filter_In in H0. intuition. destruct (lt_dec a n); simpl in *. discriminate. destruct (EqDec_dec bool_EqDec false true); intuition. rewrite allNatsLt_filter_lt. rewrite <- ratAdd_0_r. rewrite ratMult_1_r. rewrite allNatsLt_length. rewrite <- ratMult_num_den. eapply eqRat_terms. lia. unfold posnatMult, posnatToNat, natToPosnat. destruct p. lia. eapply rat_le_1_if; trivial. Qed.
imports: FCF.Crypto FCF.RndNat FCF.NotationV1