proposition: Lemma evalDist_sum_le_1 : forall (A : Set)(c : Comp A), sumList (getSupport c) (evalDist c) <= 1.
proof: Proof. induction c; intuition; simpl in *. unfold sumList; simpl in *. destruct (e a a); intuition. rewrite <- ratAdd_0_l. intuition. eapply leRat_trans. eapply eqRat_impl_leRat. apply evalDist_sum_bind_eq. eapply comp_eq_dec; eauto. eapply bind_eq_dec; eauto. eapply leRat_trans. eapply sumList_le. intuition. apply ratMult_leRat_compat. apply leRat_refl. apply H. eapply leRat_trans. eapply sumList_le; intuition. eapply eqRat_impl_leRat. eapply ratMult_1_r. trivial. rewrite sumList_body_const. rewrite getAllBvectors_length. rewrite <- ratMult_num_den. rewrite Nat.mul_1_l. eapply eqRat_impl_leRat. eapply num_dem_same_rat1. rewrite posnatMult_1_r. unfold posnatToNat, natToPosnat. trivial. destruct (gt_dec (length (filter b (getSupport c))) 0). eapply leRat_trans. eapply eqRat_impl_leRat. eapply sumList_body_eq. intuition. eapply ratMult_eqRat_compat. assert (b a = true). eapply filter_In; eauto. unfold indicator. rewrite H0. eapply ratMult_1_l. eapply eqRat_refl. eapply leRat_trans. eapply eqRat_impl_leRat. eapply ratInverse_scale_sum_1. intuition. eapply getSupport_In_evalDist. eapply filter_In. eapply H. trivial. trivial. intuition. destruct (filter b (getSupport c)); simpl in *. unfold sumList. simpl. eapply rat0_le_all. lia. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec