proposition: Lemma lowDistApprox_le_repeat: forall (n : nat) (A : Set) (c : Comp A) (P : A -> bool)(a : A) (v1 v2 : Rat), well_formed_comp c -> (exists a0 : A, In a0 (filter P (getSupport c))) -> lowDistApprox (Repeat c P) a n v1 -> lowDistApprox_repeat c P a n v2 -> n > O -> v1 <= v2.
proof: Proof. intuition. edestruct dat_exists_repeat2. eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply (repeat_low_tree_approx_same_inv); eauto. } destruct H0. edestruct dat_exists. eapply well_formed_Repeat; eauto. eapply comp_eq_dec; eauto. eapply leRat_trans. eapply eqRat_impl_leRat. symmetry. eapply low_tree_approx_same_inv. eauto. eauto. apply lowDistApprox_dat_better_le. eapply dat_repeat_better. econstructor; eauto. eapply dat_correct_repeat_same; eauto. trivial. Unshelve. eapply comp_eq_dec; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat