proposition: Lemma lowDistApprox_bind_left_total : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) a, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b)) -> left_total (lowDistApprox_bind c1 c2 a).
proof: Proof. intuition. unfold left_total. intuition. edestruct (sumList_rel_left_total). intuition. 2:{ econstructor. econstructor. eauto. } simpl. edestruct lowDistApprox_left_total. eapply bind_eq_dec; eauto. eauto. edestruct lowDistApprox_left_total. eapply comp_eq_dec; eauto. eapply H. exists (x0 * x). intuition. eapply ratMult_eqRat_compat. eapply lowDistApprox_func; eauto. eapply lowDistApprox_func. eapply H0. eauto. eauto. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat