proposition: Lemma sumList_filter_evalDist_le_1 : forall (A : Set)(c : Comp A)(P : A -> bool) a, well_formed_comp c -> In a (filter P (getSupport c)) -> 1 <= sumList (filter (fun a' => negb (P a')) (getSupport c)) (evalDist c) -> False.
proof: Proof. intuition. assert (sumList (filter (fun a0 : A => negb (P a0)) (getSupport c)) (evalDist c) == 1). eapply leRat_impl_eqRat; trivial. eapply leRat_trans. eapply sumList_filter_le. rewrite evalDist_lossless. intuition. trivial. rewrite <- evalDist_lossless in H2; eauto. rewrite (sumList_filter_partition P (getSupport c)) in H2. symmetry in H2. rewrite ratAdd_comm in H2. apply ratAdd_arg_0 in H2. eapply sumList_0 in H2; eauto. eapply getSupport_In_evalDist. eapply filter_In; eauto. trivial. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec