proposition: Lemma lowDistApprox_bind_le_div2 : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) a n r1 r2, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b)) -> lowDistApprox_bind c1 c2 a (Nat.div2 n) r1 -> lowDistApprox (Bind c1 c2) a n r2 -> r1 <= r2.
proof: Proof. intuition. edestruct (dat_exists_bind2). eauto. eauto. rewrite bind_low_tree_approx_same_inv; eauto. edestruct dat_exists. eapply well_formed_Bind; eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply low_tree_approx_same_inv. eapply H4. eapply H2. } eapply lowDistApprox_dat_better_le. apply dat_correct_bind_same in H4. eapply dat_better_bind_div2; eauto. trivial. 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