proposition: Theorem evalDist_complement : forall (c : Comp bool), well_formed_comp c -> evalDist c false == ratSubtract 1 (Pr[c]).
proof: Proof. intuition. eapply (@ratAdd_add_same_l _ (Pr[c])). rewrite ratSubtract_ratAdd_inverse_2. rewrite <- sumList_support_bool. eapply evalDist_lossless. trivial. eapply evalDist_le_1. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec