proposition: Theorem evalDist_bool_complement : forall (c : Comp bool), well_formed_comp c -> evalDist c false == ratSubtract 1 (evalDist c true).
proof: Proof. intuition. eapply (eqRat_ratAdd_same_r (evalDist c true)). symmetry. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_inverse_2. specialize (@evalDist_lossless _ c); intuition. rewrite <- H1. clear H1. eapply evalDist_bool_support. intuition. intuition. eapply evalDist_le_1. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic