proposition: Lemma lowDistApprox_le_bind : forall n (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) a r1 r2, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b)) -> lowDistApprox (Bind c1 c2) a n r1 -> lowDistApprox_bind c1 c2 a n r2 -> r1 <= r2.
proof: Proof. intuition. edestruct dat_exists_bind2. eauto. eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply (bind_low_tree_approx_same_inv). eauto. eauto. eauto. eauto. } edestruct dat_exists. eapply well_formed_Bind; eauto. eapply leRat_trans. eapply eqRat_impl_leRat. symmetry. eapply low_tree_approx_same_inv. eauto. eauto. apply lowDistApprox_dat_better_le. inversion H3; clear H3; subst. intuition. eapply datMap_depth_better. 4:{ eapply dat_correct_bind_same_h. eapply H4. eauto. trivial. intuition. eapply evalDet_steps_done_nil_inv; eauto. eauto. } eapply dat_better_refl. intuition. eapply dat_correct_dat_better. eapply H7. eapply H8. trivial. eapply H6. auto. Unshelve. eapply bind_eq_dec; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat