proposition: Theorem Bernoulli_correct_complement : forall (r : Rat), r <= 1 -> evalDist (Bernoulli r) false == ratSubtract 1 r.
proof: Proof. intuition. eapply eqRat_trans. eapply evalDist_complement. eapply Bernoulli_wf. eapply ratSubtract_eqRat_compat; intuition. eapply Bernoulli_correct. trivial. Qed.
imports: FCF.Crypto FCF.RndNat FCF.NotationV1