proposition: Lemma lowDistApprox_dat_better_le : forall (A : Set)(eqd : eq_dec A)(t1 t2 : DistApproxTree A), dat_better t1 t2 -> forall (a : A), lowDistApproxFromTree eqd t2 a <= lowDistApproxFromTree eqd t1 a.
proof: Proof. induction 1; intuition; simpl in *. apply rat0_le_all. rewrite <- IHdat_better1. rewrite <- IHdat_better2. eapply leRat_refl. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat